Best formulation for inductive propositions?

Using Coq
1

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
2

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.
3

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

4

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).

5

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