Stream: math-comp users

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


view this post on Zulip 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 => 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.

view this post on Zulip Paolo Giarrusso (Aug 06 2022 at 09:43):

f_total calls f_nodiag, not P right?

view this post on Zulip 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. 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'.

view this post on Zulip Paolo Giarrusso (Aug 06 2022 at 10:28):

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.

view this post on Zulip 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.

view this post on Zulip Notification Bot (Aug 06 2022 at 11:05):

Alex Loiko has marked this topic as resolved.

view this post on Zulip Alex Loiko (Aug 06 2022 at 11:06):

Thank you for the help, @Paolo Giarrusso


Last updated: Mar 29 2024 at 08:39 UTC