The Coq mailing list

[Robert Dockins <robdockins AT fastmail.fm>]

> I'm working my way through Coq'Art and applying the concepts to prove 
> simple 
> results from the text Types and Programming Languages.

Funny thing.  I started by proving stuff from TaPL as well.

> However I can't seem to show the remaining case.  Could someone comment on 
> how 
> to obtain this result?

As another poster mentioned, you need to show that and "If" term can
always reduce, and is thus not a normal form.

>   Also, is there an alternative formulation of 
> normal_form, mine strikes me as awkward?  

you can use "exists", but it will end up pretty much the same.  

I've attached my development of the untyped bools if you want a cheet
sheet; our definitions are pretty similar.  I don't know that I'd try to
emulate my proofs too much however -- I'm sure most of the wizards on
this list could do these proofs much more elegantly.



Require Import Omega.
Require Import List.

Inductive term : Set :=
  | TermTrue : term
  | TermFalse : term
  | TermIf : term -> term -> term -> term.

Inductive value : term -> Prop :=
  | valueT : value TermTrue
  | valueF : value TermFalse.

Fixpoint termSize (t:term) : nat :=
   match t with
   | TermTrue  => 1
   | TermFalse => 1
   | TermIf x y z => termSize x + termSize y + termSize z + 1
   end.


Reserved Notation "A --> B"  (at level 40, left associativity).
Reserved Notation "A -->* B" (at level 40, left associativity).

Inductive smallStep : term -> term -> Prop :=
   | EIfTrue  : forall (x y:term),   (TermIf TermTrue x y) --> x
   | EIfFalse : forall (x y:term),   (TermIf TermFalse x y) --> y
   | EIf      : forall (a b x y:term), (a --> b) -> (TermIf a x y) --> 
(TermIf b x y)
 where "A --> B" := (smallStep A B).

Inductive multiStep : term -> term -> Prop :=
   | BigLift  : forall x y:term, x --> y -> x -->* y
   | BigRefl  : forall x:term, x -->* x
   | BigTrans : forall x y z:term, x -->* y -> y -->* z -> x -->* z
 where "A -->* B" := (multiStep A B).

Inductive multiStepAlt : term -> term -> Prop :=
   | AltRefl  : forall x:term, multiStepAlt x x
   | AltTrans : forall x y z:term, x --> y -> multiStepAlt y z -> 
multiStepAlt x z.


Definition normalForm (t:term) : Prop := forall t1:term, ~(t --> t1).
Definition stuck (t:term) : Prop := 
    normalForm t /\ ~ value  t.


Inductive type : Set :=
   | tyBool.
   
Reserved Notation "|- A ::: B" (at level 45, no associativity).

Inductive typeJudgement : term -> type -> Prop :=
   | TTrue  : (|- TermTrue ::: tyBool)
   | TFalse : (|- TermFalse ::: tyBool)
   | TIf    : forall (t1 t2 t3:term) (ty:type), 
     |- t1 ::: tyBool ->
     |- t2 ::: ty ->
     |- t3 ::: ty -> 
     |- TermIf t1 t2 t3 ::: ty
 where "|- A ::: B" := (typeJudgement A B).

Definition wellTyped (t:term) : Prop :=
   exists ty:type, |- t ::: ty.


Lemma IfEvals : forall t1 t2 t3:term, exists x, TermIf t1 t2 t3 --> x.
Proof.
intros.
cut (t1 = TermTrue \/ t1 = TermFalse \/ (exists z : _, t1 --> z)).
 intro H.
   elim H.
  intros.
    rewrite H0.
    exists t2.
    apply EIfTrue.
  clear H.
    intro H.
    elim H.
   intros.
     rewrite H0.
     exists t3.
     apply EIfFalse.
   clear H.
     intro H.
     elim H.
     intros.
     exists (TermIf x t2 t3).
     apply EIf.
     trivial.
 induction t1.
  left.
    trivial.
  right; left; trivial.
  right; right.
    elim IHt1_1.
   intros.
     rewrite H.
     exists t1_2.
     apply EIfTrue.
   intros.
     elim H.
    clear H.
      intro H.
      rewrite H.
      exists t1_3.
      apply EIfFalse.
    clear H.
      intro H.
      elim H.
      intros.
      exists (TermIf x t1_2 t1_3).
      apply EIf.
      trivial.
Qed.



Lemma IfNotNormal : forall t1 t2 t3:term, ~(normalForm (TermIf t1 t2 t3)).
Proof.
intros.
red in |- *.
intros.
red in H.
red in H.
absurd (exists z : _, TermIf t1 t2 t3 --> z).
 red in |- *.
   intros.
   elim H0.
   apply H.
 apply IfEvals.
Qed.


Theorem DeterminacyOfEvaluation :
     forall (t t1 t2:term), (t --> t1) /\ (t --> t2) -> t1 = t2.
Proof.
intros.
elim H.
elim H.
clear H.
intro H.
generalize t2.
elim H.
 intros.
   inversion H0.
  trivial.
  inversion H7.
 intros.
   inversion H0.
  trivial.
  inversion H7.
 intros.
   inversion H2.
  rewrite <- H6 in H0.
    inversion H0.
  rewrite <- H6 in H0.
    inversion H0.
  rewrite (H1 b0 H9).
   auto.
   trivial.
   trivial.
Qed.


Theorem IfValueThenNormal :
     forall t:term, value t -> normalForm t.
Proof.
intro.
induction t.
 red in |- *.
   intros.
   inversion H.
   red in |- *.
   intro.
   inversion H0.
 intros.
   red in |- *.
   red in |- *.
   intros.
   inversion H0.
 red in |- *.
   intros.
   inversion H.
Qed.


Theorem IfNormalThenValue :
     forall t:term, normalForm t -> value t.
Proof.
intros.
induction t.
 apply valueT.
 apply valueF.
 red in H.
   red in H.
   absurd (exists z : _, TermIf t1 t2 t3 --> z).
  red in |- *.
    intros.
    elim H0.
    apply H.
  apply IfEvals.
Qed.

Theorem EquivNormalFormValue :
     forall t:term, normalForm t <-> value t.
Proof.
intro.
split.
 apply IfNormalThenValue.
 apply IfValueThenNormal.
Qed.

Lemma lemma1 : forall x y : term, ~x = TermIf TermTrue x y.
Proof.
intros x y; induction x; intros; try discriminate.
injection.
intros.
apply IHx2.
rewrite <- H0.
rewrite <- H2.
rewrite <- H1.
trivial.
Qed.

Lemma lemma2 : forall x y : term, ~y = TermIf TermFalse x y.
Proof.
intros x y; induction y; try discriminate.
injection.
intros.
apply IHy3.
rewrite <- H2.
rewrite <- H1.
rewrite <- H0.
trivial.
Qed.

Lemma SmallStepAntiReflexive : forall t:term, ~ t --> t.
Proof.
intro t; elim t.
 red in |- *; intro H; inversion H.
 red in |- *; intro G; inversion G.
 intros.
   red in |- *.
   intro G; inversion G.
  apply (lemma1 t1 t2); trivial.
  apply (lemma2 t1 t2); trivial.
  contradiction.
Qed.

Lemma SmallStepReduceSize : forall x y : term, x --> y -> (termSize x) > 
(termSize y).
Proof.
intros.
induction H.
 unfold termSize in |- *; fold termSize in |- *.
   set (u := termSize x) in |- *.
   generalize (termSize y).
   intros; omega.
 unfold termSize in |- *; fold termSize in |- *.
   set (u := termSize y) in |- *.
   generalize (termSize x).
   intros; omega.
 unfold termSize in |- *; fold termSize in |- *.
   cut (termSize a > termSize b).
  set (u := termSize x) in |- *.
    set (v := termSize y) in |- *.
    set (p := termSize a) in |- *.
    set (q := termSize b) in |- *.
    omega.
  assumption.
Qed.


Lemma SmallStepAntiSymmetric : forall t1 t2 : term, t1 --> t2 -> ~(t2 --> t1).
Proof.
intros.
red in |- *.
intros.
assert (termSize t1 < termSize t2).
 apply SmallStepReduceSize.
   assumption.
 assert (termSize t2 < termSize t1).
  apply SmallStepReduceSize; assumption.
  set (u := termSize t1) in *.
    set (v := termSize t2) in *.
    absurd (u < v).
   omega.
   assumption.
Qed.

Lemma MultiStepNonIncreasing : forall x y:term, x -->* y -> termSize x >= 
termSize y.
Proof.
intros.
induction H.
 cut (termSize x > termSize y).
  omega.
  apply SmallStepReduceSize.
    assumption.
 omega.
 omega.
Qed.


Remark MultiStepSqueeze :
   forall t1 t2:term, t1 -->* t2 -> t2 -->* t1 -> t1 = t2.
Proof.
intros.
induction H.
 inversion H0.
  absurd (x --> y).
   apply SmallStepAntiSymmetric.
     assumption.
   assumption.
  trivial.
  absurd (termSize x > termSize y).
   cut (termSize y >= termSize x).
    omega.
    apply MultiStepNonIncreasing.
      assumption.
   apply SmallStepReduceSize.
     assumption.
 trivial.
 transitivity y.
  apply IHmultiStep1.
    apply BigTrans with (y := z); assumption.
  apply IHmultiStep2.
    apply BigTrans with (y := x); assumption.
Qed.


Lemma MultiStepReflexiveIsEq :
   forall t1 t2:term, value t1 -> t1 -->* t2 -> t1 = t2.
Proof.
intros.
induction H0.
 inversion H.
  rewrite <- H1 in H0.
    inversion H0.
  rewrite <- H1 in H0.
    inversion H0.
 trivial.
 transitivity y.
  apply IHmultiStep1.
    assumption.
  apply IHmultiStep2.
    cut (value x).
   intros.
     cut (x = y).
    intros.
      rewrite <- H1.
      assumption.
    apply IHmultiStep1.
      assumption.
   assumption.
Qed.


Lemma MultiStepAltTrans : forall x y z:term, multiStepAlt x y -> multiStepAlt 
y z -> multiStepAlt x z.
Proof.
intros.
induction H.
 assumption.
 cut (multiStepAlt y z).
  intros.
    apply (AltTrans x y z).
   assumption.
   assumption.
  apply IHmultiStepAlt.
    assumption.
Qed.

Lemma MultiStepsEquiv : forall x y:term, multiStep x y <-> multiStepAlt x y.
Proof.
intros.
split.
 intros.
   induction H.
  apply (AltTrans x y y).
   assumption.
   apply AltRefl.
  apply AltRefl.
  inversion IHmultiStep1.
   rewrite <- H2.
     rewrite H2.
     assumption.
   apply (MultiStepAltTrans x y z); assumption.
 intros.
   induction H.
  apply BigRefl.
  assert (x -->* y).
   apply BigLift; assumption.
   apply (BigTrans x y z); assumption.
Qed.


Lemma AltUniqNormalForms :
      forall x y z : term,
        multiStepAlt x y -> multiStepAlt x z ->
        value y -> value z -> y = z.
Proof.
intros.
induction H.
 induction H0.
  trivial.
  inversion H1.
   rewrite <- H3 in H.
     inversion H.
   rewrite <- H3 in H.
     inversion H.
 inversion H0.
  rewrite H5 in H.
    inversion H2.
   rewrite <- H6 in H.
     inversion H.
   rewrite <- H6 in H.
     inversion H.
  assert (y = y0).
   apply (DeterminacyOfEvaluation x y y0).
     split; assumption.
   rewrite <- H8 in H5.
     apply IHmultiStepAlt; assumption.
Qed.


Theorem UniqNormalForms :
     forall t u1 u2: term,
         t -->* u1 -> t -->* u2
      -> normalForm u1 -> normalForm u2
      -> u1 = u2.
Proof.
intros.
assert (value u1).
 apply IfNormalThenValue; assumption.
 assert (value u2).
  apply IfNormalThenValue; assumption.
  assert (multiStepAlt t u1).
   cut (t -->* u1 <-> multiStepAlt t u1).
    auto.
      intros.
      elim H5.
      intros.
      apply H6.
      assumption.
    apply (MultiStepsEquiv t u1).
   assert (multiStepAlt t u2).
    cut (t -->* u2 <-> multiStepAlt t u2).
     intros.
       elim H6.
       intros.
       apply H7.
       assumption.
     apply (MultiStepsEquiv t u2).
    apply (AltUniqNormalForms t u1 u2); assumption.
Qed.

Lemma IfBigReduce : forall t1 t2 t3 x:term, multiStepAlt t1 x -> multiStepAlt 
(TermIf t1 t2 t3) (TermIf x t2 t3).
Proof.
intros.
induction H.
 apply AltRefl.
 cut (TermIf x t2 t3 --> TermIf y t2 t3).
  intros.
    apply (AltTrans (TermIf x t2 t3) (TermIf y t2 t3) (TermIf z t2 t3)); 
assumption.
  apply EIf; assumption.
Qed.

Lemma AltTerminationOfEvaluation : forall t:term, exists z:term, multiStepAlt 
t z /\ value z.
Proof.
intros.
induction t.
 exists TermTrue.
   split.
  apply AltRefl.
  apply valueT.
 exists TermFalse.
   split.
  apply AltRefl.
  apply valueF.
 elim IHt1.
   elim IHt2.
   elim IHt3.
   clear IHt1.
   clear IHt2.
   clear IHt3.
   intros.
   elim H.
   elim H0.
   elim H1.
   clear H.
   clear H0.
   clear H1.
   intros.
   induction t1.
  exists x0.
    split.
   cut (TermIf TermTrue t2 t3 --> t2).
    intros.
      apply (AltTrans (TermIf TermTrue t2 t3) t2 x0); assumption.
    apply EIfTrue.
   assumption.
  exists x.
    split.
   cut (TermIf TermFalse t2 t3 --> t3).
    intros.
      apply (AltTrans (TermIf TermFalse t2 t3) t3 x); assumption.
    apply EIfFalse.
   assumption.
  inversion H0.
   exists x0.
     split.
    rewrite <- H5 in H.
      assert
       (multiStepAlt (TermIf (TermIf t1_1 t1_2 t1_3) t2 t3)
          (TermIf TermTrue t2 t3)).
     apply (IfBigReduce (TermIf t1_1 t1_2 t1_3) t2 t3 TermTrue).
       assumption.
     assert (multiStepAlt (TermIf TermTrue t2 t3) t2).
      apply (AltTrans (TermIf TermTrue t2 t3) t2 t2).
       apply EIfTrue.
       apply AltRefl.
      assert (multiStepAlt (TermIf TermTrue t2 t3) x0).
       apply (MultiStepAltTrans (TermIf TermTrue t2 t3) t2 x0); assumption.
       apply
        (MultiStepAltTrans (TermIf (TermIf t1_1 t1_2 t1_3) t2 t3)
           (TermIf TermTrue t2 t3) x0); assumption.
    assumption.
   rewrite <- H5 in H.
     exists x.
     split.
    cut
     (multiStepAlt (TermIf (TermIf t1_1 t1_2 t1_3) t2 t3)
        (TermIf TermFalse t2 t3)).
     intros.
       cut (TermIf TermFalse t2 t3 --> t3).
      intros.
        cut (multiStepAlt (TermIf TermFalse t2 t3) x).
       intros.
         apply
          (MultiStepAltTrans (TermIf (TermIf t1_1 t1_2 t1_3) t2 t3)
             (TermIf TermFalse t2 t3) x); assumption.
       apply (AltTrans (TermIf TermFalse t2 t3) t3 x); assumption.
      apply EIfFalse.
     apply (IfBigReduce (TermIf t1_1 t1_2 t1_3) t2 t3 TermFalse); assumption.
    assumption.
Qed.


Theorem TerminationOfEvaluation : forall t:term, exists z:term, t -->* z /\ 
normalForm z.
Proof.
intros.
assert (exists z : term, multiStepAlt t z /\ value z).
 apply AltTerminationOfEvaluation.
 elim H.
   intros.
   elim H0.
   intros.
   exists x.
   split.
  cut (t -->* x <-> multiStepAlt t x).
   intros.
     elim H3.
     intros.
     apply H5.
     assumption.
   apply (MultiStepsEquiv t x).
  apply IfValueThenNormal.
    assumption.
Qed.



Theorem SubtermsWellTyped : 
  forall (t1 t2 t3:term) (ty:type),
  exists ty1:type, exists ty2:type, exists ty3:type,
     |- TermIf t1 t2 t3 ::: ty ->
     |- t1 ::: ty1 /\ |- t2 ::: ty2 /\ |- t3 ::: ty3.
intros.
exists tyBool.
exists ty.
exists ty.
intros.
inversion H.
auto.
Qed.

Theorem UniqTypes : 
  forall (t:term) (ty1 ty2:type),
   |- t ::: ty1 -> |- t ::: ty2 -> ty1 = ty2.
intros t ty1 ty2 H.
generalize ty2.
elim H.
intros.
inversion H0.
trivial.
intros.
inversion H0.
trivial.
intros.
inversion H6.
apply (H3 ty0).
assumption.
Qed.

Theorem TypedProgress :
   forall t:term, wellTyped t -> ~stuck t.
intros.
red.
intros.
inversion H.
inversion H0.
red in H3.
inversion H1.
apply H3.
rewrite <- H4.
apply valueT.
apply H3.
rewrite <- H4.
apply valueF.
rewrite <- H7 in H2.
red in H2.
red in H2.
cut (exists x:term, TermIf t1 t2 t3 --> x).
intros.
elim H9.
intros.
apply (H2 x0).
assumption.
apply IfEvals.
Qed.

Lemma CanonicalForms :
   forall v:term, 
      |- v ::: tyBool -> value v -> 
      (v = TermTrue \/ v = TermFalse).
intros.
inversion H0.
left.
trivial.
right.
trivial.
Qed.


Theorem TypedPreservation :
   forall (t1 t2:term) (ty:type),
     |- t1 ::: ty -> t1 --> t2 -> |- t2 ::: ty.
intros t1 t2 ty H.
generalize t2.
elim H.
intros.
inversion H0.
intros.
inversion  H0.
intros.
inversion H6.
rewrite <- H7.
assumption.
rewrite <- H7.
assumption.
apply TIf.
apply (H1 b).
assumption.
assumption.
assumption.
Qed.



Theorem TypeSafety :
    forall (t u:term) (ty:type),
     |- t ::: ty -> t -->* u -> ~stuck u.
intros.
red.
intros.
red in H1.
elim H1.
clear H1.
intros.
red in H2.
apply H2.
apply IfNormalThenValue.
assumption.
Qed.