Yu Zhang (May 05 2022 at 06:52): Yu Zhang (May 05 2022 at 06:52):I have the following Coq code and got stuck in simplifying the definition generated by Program Definition. Can anyone give me a hint or suggest a better way to define such structures? Thanks!
Section XXX.
Variable A : Type.
Variable B : Type.
Variable comp_b : B -> B -> option B.
Variable prop_ab : list A -> B -> Prop.
Hypothesis comp_prop:
forall a1 a2 b1 b2 b,
prop_ab a1 b1 -> prop_ab a2 b2 ->
comp_b b1 b2 = Some b -> prop_ab (a1 ++ a2) b.
Record R :=
mk_R {
R_a : list A;
R_b : B;
R_prop : prop_ab R_a R_b;
}.
Program Definition comp_r (r1 r2: R) : option R :=
match comp_b (R_b r1) (R_b r2) with
| Some b =>
Some {|
R_a := R_a r1 ++ R_a r2;
R_b := b;
|}
| None => None
end.
Next Obligation. eauto using comp_prop, R_prop. Qed.
Lemma comp_r_a (r1 r2 r: R):
comp_r r1 r2 = Some r ->
R_a r = R_a r1 ++ R_a r2.
Proof.
intros H. unfold comp_r in H.
(* destruct (comp_b (R_b r1) (R_b r2)). *)
Abort.
End XXX.
Does Unset Program Cases before the Program Definition help here?
Paolo Giarrusso (May 05 2022 at 06:56):to get the same effect locally (instead of using a flag), you can use match comp_b (R_b r1) (R_b r2) return _ with
Yu Zhang (May 05 2022 at 06:57):I just tried the flag but it seems I lost the condition to prove the obligation.
Yu Zhang (May 05 2022 at 06:58):I don't have comp_b (R_b r1) (R_b r2) = Some b anymore.
Guillaume Melquiond (May 05 2022 at 07:11):That is the kind of reasoning Coq is poorly suited for. Here is the proof:
Proof.
unfold comp_r.
generalize (@eq_refl (option B) (comp_b (R_b r1) (R_b r2))).
generalize (comp_b (R_b r1) (R_b r2)) at 1 3.
intros [o|].
I suggest you disable the display of implicit arguments and look closely at what happens at each step.
Yu Zhang (May 05 2022 at 07:14):It works like a charm. Thank you both!
Last updated: Oct 01 2023 at 19:01 UTC