# Best formulation for inductive propositions?

**URL:** <https://discourse.rocq-prover.org/t/best-formulation-for-inductive-propositions/794>\
**Category:** Using Rocq\
**Created:** [April 20, 2020, 5:45pm UTC](https://discourse.rocq-prover.org/t/best-formulation-for-inductive-propositions/794 "2020-04-20T17:45:26Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![nojb](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/nojb/32/256_2.png) [@nojb](https://discourse.rocq-prover.org/u/nojb)\
**Post date:** [April 20, 2020, 5:45pm UTC](https://discourse.rocq-prover.org/t/best-formulation-for-inductive-propositions/794/1 "2020-04-20T17:45:26Z")

</div>

Hello,

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

```auto
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:

```auto
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

---

<div class="post-metadata">

**Author:** ![Matafou](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/matafou/32/18_2.png) [@Matafou](https://discourse.rocq-prover.org/u/Matafou)\
**Post date:** [April 21, 2020, 10:44am UTC](https://discourse.rocq-prover.org/t/best-formulation-for-inductive-propositions/794/2 "2020-04-21T10:44:52Z")

</div>

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.

```auto
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.

```

---

<div class="post-metadata">

**Author:** ![nojb](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/nojb/32/256_2.png) [@nojb](https://discourse.rocq-prover.org/u/nojb)\
**Post date:** [April 21, 2020, 11:03am UTC](https://discourse.rocq-prover.org/t/best-formulation-for-inductive-propositions/794/3 "2020-04-21T11:03:51Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![Blaisorblade](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/blaisorblade/32/56_2.png) [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Post date:** [April 21, 2020, 5:37pm UTC](https://discourse.rocq-prover.org/t/best-formulation-for-inductive-propositions/794/4 "2020-04-21T17:37:21Z")

</div>

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](https://softwarefoundations.cis.upenn.edu/plf-current/UseTactics.html#lab533) (that doesn’t look like a permalink; search `applys_eq` if it breaks).

---

<div class="post-metadata">

**Author:** ![Matafou](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/matafou/32/18_2.png) [@Matafou](https://discourse.rocq-prover.org/u/Matafou)\
**Post date:** [April 21, 2020, 8:15pm UTC](https://discourse.rocq-prover.org/t/best-formulation-for-inductive-propositions/794/5 "2020-04-21T20:15:30Z")

</div>

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