# F\_equal on records generating some kind of extensionality obligation?

**URL:** <https://discourse.rocq-prover.org/t/f-equal-on-records-generating-some-kind-of-extensionality-obligation/221>\
**Category:** Using Rocq\
**Created:** [March 13, 2019, 1:59pm UTC](https://discourse.rocq-prover.org/t/f-equal-on-records-generating-some-kind-of-extensionality-obligation/221 "2019-03-13T13:59:15Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![Yannick](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/yannick/32/321_2.png) [@Yannick](https://discourse.rocq-prover.org/u/Yannick)\
**Post date:** [March 13, 2019, 1:59pm UTC](https://discourse.rocq-prover.org/t/f-equal-on-records-generating-some-kind-of-extensionality-obligation/221/1 "2019-03-13T13:59:15Z")

</div>

Dear all,  
~~I first and foremost apologize, I do not have a minimal example on hand. I hope the pattern will ring a bell to someone, and shall make my best to build one otherwise.~~  
Please see my next post for a concrete example.

I’m facing the following situation that puzzles me. Manipulating a fairly complicated record type, I want to prove equality between two such records, and hence have a goal of the form:

> {| f1 := A1; f2 := A2 |} = {| f1 := A1’; f2 := A2’ |}

Performing a **f\_equal** , I end up with the two expected equality obligations, but also a third obligation of the form:

> A1 = A1’ → A2 = A2’ → {| f1 := A1; f2 := A2 |} = {| f1 := A1’; f2 := A2’ |}

I am quite confused as to the meaning of this. Since records are merely Variants, how come that proving the equality of each of the arguments of the constructors insufficient?  
The documentation of **f\_equal** does not seem to mention anything, any pointer would hence be appreciated 🙂

Best,  
Yannick

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [March 13, 2019, 2:12pm UTC](https://discourse.rocq-prover.org/t/f-equal-on-records-generating-some-kind-of-extensionality-obligation/221/2 "2019-03-13T14:12:55Z")

</div>

> I first and foremost apologize, I do not have a minimal example on hand.  
> I hope the pattern will ring a bell to someone, and shall make my best  
> to build one otherwise.

Can we see a non-minimal example?

Gaëtan Gilbert

---

<div class="post-metadata">

**Author:** ![Yannick](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/yannick/32/321_2.png) [@Yannick](https://discourse.rocq-prover.org/u/Yannick)\
**Post date:** [March 13, 2019, 2:30pm UTC](https://discourse.rocq-prover.org/t/f-equal-on-records-generating-some-kind-of-extensionality-obligation/221/3 "2019-03-13T14:30:55Z")

</div>

Dear Gaëtan,  
I was a bit hesitant since the original code is not mine, but actually reducing it to a fairly small example was not as daunting as I thought. Here is a self-contained one, please foresee the now irrelevant names:

> Record Group := {  
> G : Type;  
> mult : G → G → G;  
> }.

> Record AsynchronousGame :=  
> {  
> P : Set;  
> X : Group;  
> action : (G X) → P → (G X) → P;  
> }.

> Definition opposite\_group (X : Group) : Group :=  
> {|  
> G := (G X) ;  
> mult m n := mult X n m;  
> |}.

> Definition dual (G: AsynchronousGame) : AsynchronousGame :=  
> {|  
> P := P G;  
> X := opposite\_group (X G);  
> action g m h := action G h m g;  
> |}.

> Lemma dual\_idempotent: forall G,  
> dual (dual G) = G.  
> Proof.  
> intros G.  
> destruct G; unfold dual; simpl.  
> f\_equal.  
> (\* Here the first goal is puzzling me \*)

Yannick

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [March 13, 2019, 2:53pm UTC](https://discourse.rocq-prover.org/t/f-equal-on-records-generating-some-kind-of-extensionality-obligation/221/4 "2019-03-13T14:53:43Z")

</div>

f\_equal gets confused because of the dependency of `action` in `P` and `X`.  
For instance if you do

```coq
Goal forall A (P:A->Type) a b c d, existT P a b = existT P c d.
  intros.
  f_equal.

```

f\_equal will have no effect because it doesn’t know how to prove such dependent equalities.  
In your case it has an effect, I guess because the dependency is not significant after reducing.

In this specific example you can prove the goal just by replacing `destruct G; unfold dual; simpl.` by `destruct G as [?[??]?];reflexivity.` (ie after you destruct the auto-named X0 the goal is trivial)

---

<div class="post-metadata">

**Author:** ![Yannick](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/yannick/32/321_2.png) [@Yannick](https://discourse.rocq-prover.org/u/Yannick)\
**Post date:** [March 13, 2019, 3:28pm UTC](https://discourse.rocq-prover.org/t/f-equal-on-records-generating-some-kind-of-extensionality-obligation/221/5 "2019-03-13T15:28:06Z")

</div>

I see. That is indeed quite clear why `f_equal` fails on dependent equality, but I got confused by the hybrid behavior in this case.  
Should it be considered as a bug in the tactic? I don’t see any case where the generated goals could be helpful.