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