Stream: Coq users

Topic: naming goals based on cases

Joachim Breitner (Dec 04 2020 at 15:11):

Thanks! This allowed me to achieve the following neat hack:

  Inductive Test :=
    | Foo: case foo, Test
    | Bar: case bar, Test.

  Goal Test -> Test.
    intros.
    destruct H; name_cases.
    [foo]: {
      named_constructor.
    }
    [bar]: {
      named_constructor.
    }
  Qed.

CaseName is isomorphic to True. The named_constructor is constructor plus discarging the CaseName obligation.

It even tries to find reasonable names for the cases when you do multiple inductions/inversions:

  Goal Test -> Test -> Test.
    intros.
    destruct H; destruct H0; name_cases.
    [foo_foo0]: {
      named_constructor.
    }
    [foo_bar]: {
      named_constructor.
    }
    [bar_foo]: {
      named_constructor.
    }
    [bar_bar0]: {
      named_constructor.
    }
  Qed.

(This relates to https://github.com/coq/coq/issues/8026 an my desire to address goals by a stable name, so that changing my Inductives doesn’t mean I have to guess which goal is which…)

Joachim Breitner (Dec 04 2020 at 15:15):

The actual implementation is horrible. A mix of Ltac1 (because I couldn't figure out how to do refine ?[H] in ltac2) and Ltac2, including character-wise string operations… It’s current state is at https://github.com/dfinity/candid/blob/40f45ab0a776284602553b3583c1df8244241953/coq/NamedCases.v, but you have been warned.

Last updated: Oct 03 2023 at 02:34 UTC