The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Selon David Van Horn 
<dvanhorn AT cs.uvm.edu>:


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

Hi David,

 Your formulation of normal_form seems to be OK. Nevertheless, since
almost all proofs of your theorem "normal_implies_value" use the
fact that any conditional expression is not in normal form, I would
prefer to first define "to be reducible", then "to be in normal form".
Moreover, the predicate "value" can be defined directly, instead of
using disjunction and equality.

Cheers,

Pierre


Inductive term : Set :=
   | ETrue  : term
   | EFalse : term
   | If  : term -> term -> term -> term.


Inductive red1 : term -> term -> Prop :=
    | E_IfTrue  : forall t2 t3 : term, (red1 (If ETrue  t2 t3) t2)
    | E_IfFalse : forall t2 t3 : term, (red1 (If EFalse t2 t3) t3)
    | E_If      : forall t1 t1': term, (red1 t1 t1') ->
                    (forall t2 t3 : term, (red1 (If t1 t2 t3) (If t1' t2 
t3))).

Hint Resolve E_IfTrue E_IfFalse E_If.

Inductive reducible (t : term) : Prop :=
 reducible_i : forall t', red1 t t' -> reducible t.

Definition normal_form t := ~(reducible t).

Inductive value  : term -> Prop :=
| val_true : value ETrue
| val_false : value EFalse.
Hint Resolve val_true val_false.

Lemma if_reducible : forall t1 t2 t3, reducible (If t1 t2 t3).
Proof.
  simple induction t1.
  intros t2 t3; exists t2 ; auto.
  intros t2 t3; exists t3; auto.
  intros t1_1 H_ind_1_1 t1_2 _ t1_3 _ t2 t3.
  case (H_ind_1_1 t1_2 t1_3);intros t' H';exists (If t' t2 t3); auto.
Qed.

Theorem normal_implies_value : forall t, normal_form t -> value t.
Proof.
 simple destruct t; auto.
 intros t0 t1 t2 H; case H.
 apply if_reducible.
Qed.




Finally, is there a more
> appropriate
> forum for asking these sorts of beginner questions?
>
> Thanks,
> David
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>


-- 
Pierre Casteran
(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.