Stream: Coq users

Topic: Simplify the definition generated by Program Definition


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

view this post on Zulip Paolo Giarrusso (May 05 2022 at 06:54):

Does Unset Program Cases before the Program Definition help here?

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

view this post on Zulip Yu Zhang (May 05 2022 at 06:57):

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

view this post on Zulip Yu Zhang (May 05 2022 at 06:58):

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

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

view this post on Zulip Yu Zhang (May 05 2022 at 07:14):

It works like a charm. Thank you both!


Last updated: Jan 27 2023 at 01:03 UTC