Best formulation for inductive propositions?


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,

1 Like

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

Lemma foobar: foo a0 (f' c0). 

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.


Best wishes,

A general applys_eq appears in Software Foundations; it has limitations, but might be interesting to consider. It’s currently described in (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.