## Stream: Coq users

### Topic: Code review / simplifying repetition

#### 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.
``````

#### Fernando Chu (Apr 18 2023 at 19:25):

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').
``````

#### Fernando Chu (Apr 18 2023 at 23:05):

nicer indeed, thanks again.

Last updated: Jun 25 2024 at 18:02 UTC