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?

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`

?

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.

(every other definition is according to this)

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: Jun 25 2024 at 18:02 UTC