Stream: Coq users

Topic: Reduce goals to only nontrivial ones


view this post on Zulip Audrey Seo (Sep 26 2023 at 01:32):

Hi everyone, I have some inductive types for props whose proofs I'd like to automate, and hopefully without making coq take forever.

Suppose I have a grammar:

Inductive cmd :=
| Skip
| Assign (x: string) (v: nat)
| Seq (c1 c2: cmd).

And some kind of defined, not exactly nontrivial propositions:

Definition cmd_prop (c: cmd) (n: nat) (l: list string): Prop := ... .

And an inductive definition like this one:

Inductive foo : cmd -> nat -> list string  -> Prop :=
| SkipFoo :
  forall (n: nat) (l: list string),
    foo Skip n l
| AssignFoo :
  forall (n: nat) (l: list string) (x: string) (v: nat),
    cmd_prop (Assign  x v) n l ->
    foo (Assign x v) n l
| SeqFoo :
  forall (n: nat) (l: list string) (c1 c2: cmd),
    cmd_prop (Seq c1 c2) n l ->
    foo c1 n l ->
    foo c2 n l ->
    foo (Seq c1 c2) n l.

My use case is that I would like to automatically reduce foo c n l for concrete c, n, and l to just the cmd_prop cases.

With simpler inductive types, I would have just used reflection and written a fixpoint definition that returns option (foo c n l), then made a tactic that tried to unwrap the option and would prove the goal if it found Some. But I can't figure out a way to do that in this case, due to the "not exactly nontrivial" nature of cmd_prop.

Is my best bet just to write some custom ltac that calls econstructor on every foo goal generated, leaving the cmd_prop goals, or is there something more efficient/effective that I could do?


Last updated: Jun 23 2024 at 03:02 UTC