Hi, I have a dependent types issue in mathcomp. I'm not sure whether this is the right forum to ask for help, but here comes:

I want to prove this:

```
1 goal (ID 832)
T : finType
f_nodiag : forall u v : T, u != v -> T
u, v, x : T
e : u != v
============================
f_nodiag u v e =
match
(if u != v as b return (reflect b b)
then ReflectT true is_true_true
else ReflectF false not_false_is_true)
with
| ReflectT _ e0 => f_nodiag u v e0
| ReflectF _ _ => x
end
```

For context, `f_nodiag`

is a function of two arguments that is defined for all `T×T`

except the diagonal, and I want to make it a total function by returning the default value `x`

for `u, v`

that are equal. I've defined the extended version as

```
Definition f_total (T: finType) (f_nodiag : (forall (u v: T) (e: u != v), T)):
(forall (u v x: T), T) :=
fun u v x =>
match (@idP (u != v)) with
| ReflectT e => f_nodiag u v e
| ReflectF _ => x
end.
```

and want to prove that it agrees with the original one:

```
Lemma f_total_agrees_with_f (T: finType)
(f_nodiag : (forall (u v: T) (e: u != v), T)):
forall (u v x: T) (e: u != v),
f_nodiag u v e = (f_total f_nodiag u v x).
```

Then I got stuck because of all the dependent types. I've tried `hammer`

and `sauto`

which failed.

For a broader context, I want to show that this statement of something called the Friendship theorem implies a shorter one:

```
(* more verbose version *)
Theorem Friendship
(T: finType) (T_nonempty: [set: T] != set0)
(F (* friendship relation *): rel T) (Fsym: symmetric F) (Firr: irreflexive F)
(Co: T -> T -> T) (Col: forall u v : T, u != v -> F u (Co u v))
(Cor: forall u v : T, u != v -> F v (Co u v))
(CoUnique: forall u v w : T, u != v -> F u w -> F v w -> w = Co u v):
{u : T | forall v : T, u != v -> F u v}.
```

```
(* shorter version *)
Theorem Friendship2
(T: finType) (T_nonempty: [set: T] != set0)
(F (* friendship relation *): rel T) (Fsym: symmetric F) (Firr: irreflexive F) :
(* u!= v have exactly 1 common friend *)
(forall (u v: T), u != v -> #|[set w | F u w & F v w]| = 1) ->
{u : T | forall v : T, u != v -> F u v}.
```

From the term with type `(forall (u v: T), u != v -> #|[set w | F u w & F v w]| = 1)`

I want to recreate the 4 terms with `Co`

in their names

```
Record CoSpec (T: finType) :=
CoSpecR {
F: rel T;
Co: T -> T -> T;
Col: forall u v : T, u != v -> F u (Co u v);
Cor: forall u v : T, u != v -> F v (Co u v);
CoUnique: forall u v w : T, u != v -> F u w -> F v w -> w = Co u v
}.
Lemma construct_co (T: finType) (T_nonempty: [set: T] != set0)
(F (* friendship relation *): rel T) (Fsym: symmetric F) (Firr: irreflexive F) :
(forall (u v: T), u != v -> #|[set w | F u w & F v w]| = 1) ->
CoSpec T.
```

f_total calls f_nodiag, not P right?

Sorry, yes, I renamed 'P' into f_nodiag after pasting from Coq and missed one. Now edited. I realized that I didn't include the lemma that gave the proof state. Full Coq code that ends in the proof state follows:

```
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Definition idP' :=
fun b1 : bool =>
if b1 as b return (reflect b b)
then ReflectT true is_true_true
else ReflectF false not_false_is_true.
Definition f_total (T: finType) (f_nodiag : (forall (u v: T) (e: u != v), T)):
(forall (u v x: T), T) :=
fun u v x =>
match (@idP' (u != v)) with
| ReflectT e => f_nodiag u v e
| ReflectF _ => x
end.
Lemma f_total_agrees_with_f (T: finType)
(f_nodiag : (forall (u v: T) (e: u != v), T)):
forall (u v x: T) (e: u != v),
f_nodiag u v e = (f_total f_nodiag u v x).
Proof. move=> u v e; rewrite /f_total /idP'.
```

Here's one way. See comments:

```
Lemma f_total_agrees_with_f (T: finType)
(f_nodiag : (forall (u v: T) (e: u != v), T)):
forall (u v x: T) (e: u != v),
f_nodiag u v e = (f_total f_nodiag u v x).
Proof.
move=> u v x; rewrite /f_total /idP'.
(* This failure is instructive: you can't rewrite a subterm [t] when
abstracting [t] is ill-typed, you must abstract things to reduce typing constraints. *)
Fail move: (u != v).
move: (f_nodiag u v) => {}f_nodiag.
(* Probably doable via ssreflect dependent case, but that's more manual and I
haven't tried. *)
destruct (u != v) => // e.
by rewrite (bool_irrelevance is_true_true e).
Qed.
```

tweaked further:

```
Proof.
move=> u v x; rewrite /f_total /idP'.
(* This failure is instructive: you can't rewrite a subterm [t] when
abstracting [t] is ill-typed, you must abstract things to reduce typing constraints. *)
Fail move: (u != v).
move: (f_nodiag u v) => {f_nodiag}.
case: (u != v) => // f' e.
by rewrite (bool_irrelevance is_true_true e).
Qed.
```

Alex Loiko has marked this topic as resolved.

Thank you for the help, @Paolo Giarrusso

Last updated: Jul 25 2024 at 15:02 UTC