Stream: Coq users

Topic: use of same command


view this post on Zulip zohaze (May 01 2023 at 06:09):

destruct (PeanoNat.Nat.eqb_spec x1 x2) as [->|Dx1x2].
Want to apply it on another data type

Definition mass (m1 m2: mas) : bool :=
 match m1, m2 with
 | lit, lit => true
 | med, med => true
 | larg, larg => true
 | _, _ => false
 end.

But it not does not replace m1 with m2. Therefore i am unable to simplify it further.

view this post on Zulip Laurent Théry (May 01 2023 at 07:34):

you should prove the equivalent of eq_spec

Definition mass (m1 m2: mas) : bool :=
 match m1, m2 with
 | lit, lit => true
 | med, med => true
 | larg, larg => true
 | _, _ => false
 end.

Lemma mas_spec x y : reflect (x = y) (mass x y).
Proof.
destruct x; destruct y; simpl; constructor; auto; try discriminate.
Qed.

Goal forall (P: mas -> Prop) x y, P x -> P y.
Proof.
intros P x y.
destruct (mas_spec x y) as [-> | xDy].

view this post on Zulip zohaze (May 01 2023 at 15:13):

Thank u.


Last updated: Jun 24 2024 at 14:01 UTC