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?

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`

I just tried the flag but it seems I lost the condition to prove the obligation.

I don't have `comp_b (R_b r1) (R_b r2) = Some b`

anymore.

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.

It works like a charm. Thank you both!

Last updated: Jun 18 2024 at 22:01 UTC