Fernando Chu (Apr 18 2023 at 16:37): Fernando Chu (Apr 18 2023 at 16:37):Hello, I'm practicing with Coq, and I wrote this proof of confluence for the type theory presented here. However, the proof is long, and other than 4 uses of the inductive hypothesis, all the other cases come from inversion, rewriting, using exfalso and using one of 4 previous normalization lemmas.
How could I improve/shorten the proof?
Laurent Théry (Apr 18 2023 at 18:46):Difficult to review without being able to replay the proof. A first improvment is to understand why you need so many exfalso and exists .... What is the statement of true_normal_form?
Fernando Chu (Apr 18 2023 at 19:24):Thanks. Here are the omitted lemmas.
Definition normal_form (t : tm) : Prop := ~ exists t', t --> t'.
Lemma true_normal_form : normal_form <{ true }>.
Proof. unfold normal_form, not. intros. inversion H. inversion H0. Qed.
Lemma false_normal_form : normal_form <{ false }>.
Proof. unfold normal_form, not. intros. inversion H. inversion H0. Qed.
Lemma zero_normal_form : normal_form <{ 0 }>.
Proof. unfold normal_form, not. intros. inversion H. inversion H0. Qed.
Lemma succ_nvalue_normal_form (v : tm) : nvalue v -> normal_form <{ succ v }>.
Proof.
induction v; intros; unfold normal_form, not; intros; inversion H; inversion H0; auto.
- inversion H1. inversion H3.
- apply IHv; auto. inversion H3. exists t1'. auto.
Qed.
so I need to tell Coq that the one of the hypothesis introduced by inversion is impossible, since it was already a normal form.
Fernando Chu (Apr 18 2023 at 19:26):(every other definition is according to this)
Laurent Théry (Apr 18 2023 at 21:34):If you define
Definition normal_form (t : tm) : Prop := forall t', ~ (t --> t').
Then
exfalso. apply true_normal_form. exists c'. apply H4.
becones
now destruct (true_normal_form c').
nicer indeed, thanks again.
Last updated: Sep 23 2023 at 07:01 UTC