F_equal on records generating some kind of extensionality obligation?

Using Coq
1

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 :slight_smile:

Best,
Yannick

2

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

3

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

4

f_equal gets confused because of the dependency of action in P and X.
For instance if you do

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)

5

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.