## Stream: math-comp users

### Topic: Dependent types: total functions from #|[set w | P w]|=1

#### Alex Loiko (Aug 06 2022 at 07:03):

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 => P u v e
| ReflectF _ => x
end.
``````

and want to prove that it agrees with the original one. 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.
``````

#### Paolo Giarrusso (Aug 06 2022 at 09:43):

f_total calls f_nodiag, not P right?

#### Alex Loiko (Aug 06 2022 at 09:56):

Sorry, yes, I renamed 'P' into f_nodiag after pasting from Coq and missed one. Now edited.

#### Paolo Giarrusso (Aug 06 2022 at 10:28):

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

#### Paolo Giarrusso (Aug 06 2022 at 10:33):

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

Last updated: Feb 08 2023 at 07:02 UTC