coq中范式的定义

Question

在 B. Pierce 的《Types and Programming Languages》一书中，作者介绍了一种小语言，以介绍本书中使用的不同概念。

语言如下：

t::=
    true
    false
    if t then t else t
v::=
    true
    false

一共有三个归约规则：

if true then t2 else t3 \rightarrow t2

if false then t2 else t3 \rightarrow t3

t1 \rightarrow t1'
------------------
if t1 then t2 else t3 \rightarrow if t1' then t2 else t3

我想证明每个范式都是一个值。

我对范式使用以下定义：

Definition normal_form (t:term) :=
  ~(exists t',  step t t').

我卡住了，因为在某一时刻，我有一些东西看起来像：

~ ~(exists t : term, ...)

我不知道如何推断

exists t : term, ...

因为我们处于直觉逻辑中。

这是完整的证明：

Inductive term : Set :=
| true : term
| false : term
| ifthenelse : term -> term -> term -> term.


Definition normal_form (t:term) :=
  ~(exists t',  step t t').

Inductive is_value : term -> Prop :=
| vtrue : is_value true
| vfalse : is_value false.


Lemma normal_form_implies_value : forall t, normal_form t -> is_value t.
Proof.
  intro.
  induction t.
  intros.
  apply vtrue.
  intros.
  apply vfalse.
  intros.
  unfold normal_form in H.
  destruct t1.
  unfold not in H.
  assert (exists t' : term, step(ifthenelse true t2 t3) t').
  exists t2.
  apply eiftrue.
  apply H in H0.
  contradiction.
  assert (exists t' : term, step(ifthenelse false t2 t3) t').
  exists t3.
  apply eiffalse.
  apply H in H0.
  contradiction.
  assert(~(is_value (ifthenelse t1_1 t1_2 t1_3))).
  intro.
  inversion H0.
  assert(~(normal_form(ifthenelse t1_1 t1_2 t1_3))).
  intro.
  apply IHt1 in H1.
  contradiction.
  unfold normal_form in H1.
  unfold not in H1.

我应该为范式使用其他定义吗？没有任何经典公理是否可以完成证明？

Answer 1

要证明的一个有趣的引理是反演引理，它指出如果 ifthenelse b l r 是正规形式，那么 b、l 和 r 也是正规形式。

Lemma normal_form_ifthenelse (b l r : term) :
  normal_form (ifthenelse b l r) ->
  normal_form b /\ normal_form l /\ normal_form r.

如果您愿意使用自动化机器的大量帮助，可以很容易地证明这一点。

Proof.
   intros H        (* assumption "normal_form (ifthenelse b l r)" *)
 ; repeat split    (* split the big conjunction into 3 goals *)
 ; intros [t redt] (* introduce the "exists t',  step t t'" proofs
                      all the goals are now "False" *)
 ; apply H         (* because we know that "step t t'", we are going to
                      be able to prove that "step (ifthenelse ...) ..."
                      which H says is impossible *)
 ; eexists         (* we let Coq guess which term we are going to step to *)
 ; constructor     (* we pick the appropriate constructor between the structural ones *)
 ; eapply redt.    (* finally we lookup the proof we were given earlier *)
Qed.

如果这对您来说过于自动化，您可以尝试手动证明以下（更简单的）引理，因为这是我们在最终证明中需要的部分：

Lemma normal_form_ifthenelse (b l r : term) :
  normal_form (ifthenelse b l r) -> normal_form b.

然后可以相当快地证明你的引理：在归纳的前两个情况中，使用 constructor 将选择正确的 is_value 构造函数。

在最后一个中，我们得到了一个归纳假设IHt1，它说如果t1是一个normal_form那么它就是is_value。我们可以使用我们的中间引理根据我们知道 normal_form (ifthenelse t1 t2 t3) 的事实来证明 normal_form t1 并得出 is_value t1.

但是 t1 是一个值的事实与 normal_form (ifthenelse t1 t2 t3) 的事实相矛盾：我们确实可以根据 t1 是 true 或 false。 False_ind 是我们说 "and now we have derived a contradiction".

的一种方式

Lemma normal_form_implies_value : forall t, normal_form t -> is_value t.
Proof.
intro t; induction t; intro ht.
  - constructor.
  - constructor.
  - destruct (normal_form_ifthenelse _ _ _ ht) as [ht1 _].
    apply False_ind, ht; destruct (IHt1 ht1); eexists; constructor.
Qed.

Answer 2

is_value可判定，

Lemma is_value_dec : forall t, {is_value t} + {~is_value t}.
Proof.
    induction t;
    try (left; constructor);
    destruct IHt1;
    right; intro C; inversion C.
Qed.

所以你可以通过考虑这两种情况（destruct）来证明normal_form_implies_value，就像这样：

Lemma normal_form_implies_value : forall t, normal_form t -> is_value t.
Proof.
    induction t;
    try constructor;
    intros;
    destruct (is_value_dec t1), t1;
    apply False_ind;
    apply H;
    try (eexists; constructor; fail);
    try (inversion i; fail).
    contradict n;
    apply IHt1;
    intros [tt C];
    eauto using scomp.
Qed.

scomp 是 step 的构造函数，使用这个定义：

Inductive step : term -> term -> Prop :=
| strue:  forall t1 t2, step (ifthenelse true  t1 t2) t1
| sfalse: forall t1 t2, step (ifthenelse false t1 t2) t2
| scomp: forall t1 t1' t2 t3, step t1 t1' -> 
          step (ifthenelse t1 t2 t3) (ifthenelse t1' t2 t3).

coq中范式的定义

Definition of normal form in coq

normalization

coq