Stream: Coq users

Topic: Code review / simplifying repetition


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Fernando Chu (Apr 18 2023 at 19:26):

(every other definition is according to this)

view this post on Zulip 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').

view this post on Zulip Fernando Chu (Apr 18 2023 at 23:05):

nicer indeed, thanks again.


Last updated: Jun 25 2024 at 18:02 UTC