Sometimes I need to define an inductive proposition of the following form:

Inductive foo : A -> B -> Prop :=
| Foo : forall c, foo a0 (f c).

where a0 : A and f : C -> B.

The issue is that when trying to prove a statement of the form foo a b if I want to apply Foo I need to first assert that a = a0 and b = f c for some c. Is there a way to “apply” Foo and automatically deduce new goals with the required equalities ?

I could include the equalities in the definition of the inductive type, as in:

Inductive foo : A -> B -> Prop :=
| Foo : forall a b c,
a = a0 ->
b = f c ->
foo a b.

but this feels very inelegant. Is there another way?

Hi,
I don’t feel this particularly inelegant with the equalities but you can define a tactic which first assert that the actual parameters of foo are actually equal to the expected ones. Not sure it is worth it.

Section Foo.
Variable A B C:Type.
Variable c0:C.
Variable a0:A.
Variable f: C -> B.
Variable f': C -> B.
Inductive foo : A -> B -> Prop :=
| Foo : forall c, foo a0 (f c).
Ltac apply_foo :=
match goal with
| |- foo ?X ?Y =>
let hx := fresh "hx" in
let hy := fresh "hy" in
assert (hx:X = a0);
[
| try rewrite hx;
assert (hy:exists d, Y = f d);
[
| destruct hy as [d hy];
try rewrite hy;
apply Foo
]
]
end.
Lemma foobar: foo a0 (f' c0).
Proof.
apply_foo.

Thanks for the tactic idea. In my actual case, the inductive type has many such cases and adding the necessary equalities for each one of them is adds quite a bit of “noise.” I think defining a suitable tactic may be useful.