zohaze (May 01 2023 at 06:09): 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.
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].
Thank u.
Last updated: Oct 04 2023 at 21:01 UTC