# Best formulation for inductive propositions?

Hello,

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?

Any suggestions appreciated. Thanks!

Best wishes,
Nicolás

1 Like

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.

Thanks!

Best wishes,
Nicolás

A general `applys_eq` appears in Software Foundations; it has limitations, but might be interesting to consider. It’s currently described in https://softwarefoundations.cis.upenn.edu/plf-current/UseTactics.html#lab533 (that doesn’t look like a permalink; search `applys_eq` if it breaks).

I am not aware of a tactic anything automating this, but that could be worth a feature request to coq team.