Stream: Coq users

Topic: ✔ Bijection between (fin n) and (fin m) implies n=m

view this post on Zulip zaa (Apr 17 2022 at 19:28):

Require Import Utf8 Lia.
Set Implicit Arguments.

Definition fin n := { i | i < n }.
Definition bijection A B := ∃ (f: A → B) (g: B → A), (∀ x, g (f x) = x) ∧ (∀ y, f (g y) = y).

Theorem bijection_between_fins n m: bijection (fin n) (fin m) → n = m.
Proof.
Admitted.

How to prove the theorem? Any suggestions?
My approach was such that I reached situation with hypothesis bijection (S n) (S m) and goal bijection n m, but I got lost when I tried to destruct the first bijection and define explicit functions f and g for the second (probably because I'm muddle headed).

view this post on Zulip zaa (Apr 18 2022 at 16:25):

For now my try is unsuccesful. Even if it would work the potential result is going to be something disgusting...

Is there some different way to define bijection between types, maybe?

view this post on Zulip Li-yao (Apr 18 2022 at 16:31):

from f : fin (S n) -> fin (S m) first try to define f_ : fin n -> nat, to be used as the first component of the eventual function f' : fin n -> fin m.

view this post on Zulip Paolo Giarrusso (Apr 18 2022 at 17:12):

I agree with @zaa, a direct proof seems nasty: you'd have to reorder the range of f appropriately.
stdpp has a proof of this theorem that seems to bypass this step altogether: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/finite.v#L152-153.

view this post on Zulip Paolo Giarrusso (Apr 18 2022 at 17:16):

I haven't studied the proof in detail, but here's an idea (which might relate to what is going on): trychotomy lets you decide whether n < m, n = m or m < n; if n = m we're done, else we can proceed by contradiction. bijection is symmetric (exercise), so without loss of generality we can focus on n < m -> bijection (fin n) (fin m) -> False.

view this post on Zulip Paolo Giarrusso (Apr 18 2022 at 17:23):

OTOH, what's left is essentially a variant of the pigeonhole theorem (also available in that file, and left as an exercise in https://softwarefoundations.cis.upenn.edu/lf-current/IndProp.html with a different formulation)

view this post on Zulip Meven Lennon-Bertrand (Apr 18 2022 at 18:06):

On top of rearranging the range, you’d also have to prove that two subset types are equal (in the section/retraction equations), which is quite a lot of pain! Although in this case you should be lucky because I think you can prove that n < m has at most one proof.

view this post on Zulip zaa (Apr 18 2022 at 19:38):

Thank you! I will go study the proof of stdpp.

view this post on Zulip Paolo Giarrusso (Apr 18 2022 at 20:02):

@Meven Lennon-Bertrand ah, you mean the elements of subset types are equal

view this post on Zulip Paolo Giarrusso (Apr 18 2022 at 20:03):

I agree, but that’s a lemma you want anyway to use this fin, IMHO.

view this post on Zulip Paolo Giarrusso (Apr 18 2022 at 20:06):

I think it’s true as you say, but if it isn’t, you can always turn to Nat.ltb i n = true or similar constructions (in stdpp we write bool_decide (i < n) = true); proof irrelevance there is provable. But I haven’t learned these tricks from, say, software foundations.

view this post on Zulip Gaëtan Gilbert (Apr 18 2022 at 22:14):

foo.v
here is a 150 line + stdlib proof
considering stdpp uses 

Class Finite A `{EqDecision A} := {
  enum : list A;
  (* [NoDup] makes it easy to define the cardinality of the type. *)
  NoDup_enum : NoDup enum;
  elem_of_enum x : x ∈ enum
}.

its proof is probably similar but less adhoc

view this post on Zulip Notification Bot (Apr 19 2022 at 07:31):

Bas Spitters has marked this topic as resolved.

view this post on Zulip Notification Bot (Apr 19 2022 at 07:31):

Bas Spitters has marked this topic as unresolved.

view this post on Zulip Meven Lennon-Bertrand (Apr 19 2022 at 07:46):

Gaëtan Gilbert said:

here is a 150 line + stdlib proof

But it’s a proof for Fin.t, right? This is likely easier than fin defined as a subset type? But indeed you probably want to use that finite type rather than the subset one, if possible

view this post on Zulip Gaëtan Gilbert (Apr 19 2022 at 09:11):

not especially hard to go between

Definition fin n := { i | i < n }.

Lemma fin_fin'_bij n : @Bijective (Fin.t n) (fin n) (@to_nat n).
Proof.
  exists (fun x:fin n => of_nat_lt (proj2_sig x)).
  split.
  - apply of_nat_to_nat_inv.
  - intros x. rewrite to_nat_of_nat. destruct x;reflexivity.
Qed.

view this post on Zulip Paolo Giarrusso (Apr 19 2022 at 10:16):

@Meven Lennon-Bertrand mathcomp uses a subset type to replace vector, why not for fin?

view this post on Zulip Karl Palmskog (Apr 19 2022 at 10:19):

yet another "first-order" fin encoding: https://github.com/uwplse/StructTact/blob/master/theories/Fin.v

view this post on Zulip Paolo Giarrusso (Apr 19 2022 at 12:25):

Hm, I guess the argument for subset types is that you get to reuse the theory on the base type + arbitrary tactics to solve the obligations...

view this post on Zulip Notification Bot (Apr 20 2022 at 08:22):

zaa has marked this topic as resolved.

view this post on Zulip Notification Bot (Apr 20 2022 at 18:17):

zaa has marked this topic as unresolved.

view this post on Zulip zaa (Apr 20 2022 at 18:25):

Once again, big thank you for your answers, especially Gaëtan Gilbert.

Anyway, the nasty way of proving the theorem (which still fascinates me but I can't make to work) is messing with my brain and making me very frustrated. :\ :D Is there some way to put the bounty on direct proof (the nasty one) of the following theorem? I have more important things (studies, exam tomorrow etc.) to do for now and I'm ready to pay some money for the proof. I really hope this isn't impolite or smth.

(Proof irrelevance for le can be assumed without proof because it can be found on the internet, I believe. And there's the "transparent assert" tactic, which could be useful: Tactic Notation "transparent" "assert" "(" ident(H) ":" open_constr(type) ")" := refine (let H := (_: type) in _). I have forgotten where I have found this one, but it was Internet too. )

Require Import Utf8 Lia.
Set Implicit Arguments.

Definition fin n := { i | i < n }.
Definition bijection A B := ∃ (f: A → B) (g: B → A), (∀ x, g (f x) = x) ∧ (∀ y, f (g y) = y).

Theorem bijection_between_fins_aux n m: bijection (fin (S n)) (fin (S m)) → bijection (fin n) (fin m).
Proof.
Admitted.

view this post on Zulip Gaëtan Gilbert (Apr 20 2022 at 21:11):

(with Notation "X <~> Y" := (bijection X Y))
it should be easy to prove (fin (S n)) <~> option (fin n)
the problem then reduces to (option A <~> option B) -> A <~> B which came up on coq club a while ago
I don't remember if a proof ever got posted
we could even generalize further to ((A + B) <~> (A + C)) -> B <~> C (with option A <~> unit + A)
EDIT actually that only works with finite A so the option theorem is more primitive

view this post on Zulip zaa (Apr 20 2022 at 21:30):

I am two tiny admits away from proving the theorem with the direct/nasty approach and hope to finish before falling asleep. If I'm successful this night, I will post cleared up version of the proof tomorrow evening.

view this post on Zulip zaa (Apr 20 2022 at 21:43):

It's done... now clearing up the unholy mess.

view this post on Zulip zaa (Apr 20 2022 at 22:43):

Require Import Utf8 Lia Arith.
Set Implicit Arguments.

Definition fin n := { i | i < n }.
Definition bijection A B := ∃ (f: A → B) (g: B → A), (∀ x, g (f x) = x) ∧ (∀ y, f (g y) = y).

Theorem le_PI n m (A B: le n m): A = B.
Proof.
Admitted.

Coercion fin_proj1 n (f: fin n) := proj1_sig f.

Theorem fin_aux n (f1 f2: fin n): fin_proj1 f1 = fin_proj1 f2 → f1 = f2.
Proof.
  intros. destruct f1, f2. simpl in *. subst. f_equal. apply le_PI.
Qed.

Tactic Notation "transparent" "assert" "(" ident(H) ":" open_constr(type) ")" :=
  refine (let H := (_: type) in _).

Theorem bijection_between_fins_aux n m: bijection (fin (S n)) (fin (S m)) → bijection (fin n) (fin m).
Proof.
  intros [f [g [H H0]]].
  transparent assert (f0:(fin n → fin m)). Unshelve.
  2:{ intros [x Hx]. assert (x < S n) by auto. assert (n < S n) by auto.
      exists (if le_lt_dec (f (exist _ n H2)) (f (exist _ x H1))
              then f (exist _ x H1) - 1
              else f (exist _ x H1)).
      destruct le_lt_dec.
      + abstract (
          remember (f (exist _ x H1)) as W; remember (f (exist _ n H2)) as W0;
          destruct W, W0; simpl in *;
          assert (x0 ≠ 0) by (
            intro; subst; assert (x1 = 0) by abstract lia; subst; clear l;
            assert (l0 = l1) by apply le_PI; subst;
            rewrite HeqW in HeqW0; assert (x ≠ n) by abstract lia;
            assert (exist (λ i, i < S n) x H1 ≠ exist _ n H2) by (intro; apply H3; inversion H4; auto);
            assert (f (exist _ x H1) ≠ f (exist _ n H2)) by (intro; apply H4; rewrite <- H; rewrite <- H at 1; f_equal; auto);
            auto);
          abstract lia).
      + abstract (destruct (f (exist _ x H1)), (f (exist _ n _)); simpl in *; abstract lia). }
  transparent assert (g0:(fin m → fin n)). Unshelve.
  2:{ clear f0. intros [x Hx]. assert (x < S m) by auto.
      assert (n < S n) by auto. assert (S x < S m) by intuition.
      exists (if le_lt_dec (f (exist _ n H2)) x
              then g (exist _ (S x) H3)
              else g (exist _ x H1)).
      destruct le_lt_dec.
      + abstract (
          assert (g (exist _ (S x) H3) ≠ exist _ n H2) by (intro; rewrite <- H4, H0 in l; simpl in l; abstract lia);
          assert (fin_proj1 (g (exist _ (S x) H3)) ≠ n) by (intro; apply H4; apply fin_aux; simpl; auto);
          assert (fin_proj1 (g (exist _ (S x) H3)) < S n) by (destruct (g (exist _ _ _)); simpl; auto);
          abstract lia).
      + abstract (
          assert (g (exist _ x H1) ≠ exist _ n H2) by (intro; rewrite <- H4, H0 in l; simpl in l; abstract lia);
          assert (fin_proj1 (g (exist _ x H1)) ≠ n) by (intro; apply H4; apply fin_aux; simpl; rewrite <- H5; auto);
          assert (fin_proj1 (g (exist _ x H1)) < S n) by (destruct (g (exist _ _ _)); simpl; auto);
          abstract lia). }
      exists f0, g0; unfold f0, g0; clear f0 g0. split; intros.
      * destruct x. apply fin_aux. simpl. repeat destruct le_lt_dec.
        ++ assert (let w := fin_proj1 (f (exist _ x (le_S (S x) n l))) in w = 0 ∨ w > 0) by abstract lia.
           destruct H1.
           ** rewrite H1 in l0. assert (fin_proj1 (f (exist _ n (le_n (S n)))) = 0) by abstract lia.
              assert (f (exist (λ i, i < S n) x (le_S (S x) n l)) = f (exist _ n (le_n (S n)))).
              { assert (0 < S m) by abstract lia.
                assert (f (exist _ x (le_S (S x) n l)) = exist _ 0 H3).
                { apply fin_aux. rewrite H1. auto. }
                assert (f (exist _ n (le_n (S n))) = exist _ 0 H3).
                { apply fin_aux. rewrite H2. auto. }
                congruence. }
              assert (x = n).
              { assert (exist (λ i, i < S n) x (le_S (S x) n l) = exist _ n (le_n (S n))).
                { rewrite <- H. rewrite <- H at 1. f_equal. auto. }
                inversion H4. auto. }
              abstract lia.
           ** assert (S (f (exist _ x (le_S (S x) n l)) - 1) = f (exist _ x (le_S (S x) n l))) by abstract lia.
              assert (∀ (w: fin (S n)) (H: f w > 0) (H0: S (f w - 1) < S m), g (exist _ (S (f w - 1)) H0) = w).
              { intros. assert (S (fin_proj1 (f w) - 1) = fin_proj1 (f w)) by abstract lia.
                rewrite <- (H w). f_equal. apply fin_aux. simpl. auto. }
              rewrite H3. auto. auto.
        ++ exfalso. assert (fin_proj1 (f (exist _ x (le_S (S x) n l))) = fin_proj1 (f (exist _ n (le_n (S n))))) by abstract lia.
           assert (f (exist _ x (le_S (S x) n l)) = f (exist _ n (le_n (S n)))).
           { apply fin_aux. auto. }
           assert (exist (λ i, i < S n) x (le_S (S x) n l) = exist _ n (le_n (S n))).
           { rewrite <- H. rewrite <- H at 1. f_equal. auto. }
           inversion H3. abstract lia.
        ++ exfalso. assert (fin_proj1 (f (exist _ n (le_n (S n)))) = fin_proj1 (f (exist _ x (le_S (S x) n l)))) by abstract lia.
           assert (f (exist _ n (le_n (S n))) = f (exist _ x (le_S (S x) n l))).
           { apply fin_aux; auto. }
           assert (exist (λ i, i < S n) n (le_n (S n)) = exist _ x (le_S (S x) n l)).
           { rewrite <- H. rewrite <- H at 1. f_equal. auto. }
           inversion H3. abstract lia.
        ++ clear l0. assert (∀ (w: fin (S n)) (H: fin_proj1 (f w) < S m), g (exist _ (fin_proj1 (f w)) H) = w).
           { intros. rewrite <- H. f_equal. apply fin_aux. simpl. auto. }
           rewrite H1. simpl. auto.
      * assert (∀ (w: fin (S m)) (H: fin_proj1 (g w) < S n), f (exist _ (fin_proj1 (g w)) H) = w).
        { intros. rewrite <- H0. f_equal. apply fin_aux. simpl. auto. }
        destruct y. apply fin_aux. simpl. repeat destruct le_lt_dec.
        ++ rewrite H1. simpl. abstract lia.
        ++ exfalso. rewrite H1 in l0. simpl in l0. abstract lia.
        ++ exfalso. rewrite H1 in l0. simpl in l0. abstract lia.
        ++ rewrite H1. simpl. auto.
Qed.

Theorem bijection_between_fins n m: bijection (fin n) (fin m) → n = m.
Proof.
  revert n. induction m.
  + intros n [f [g [H H0]]]. destruct n; auto. exfalso. destruct (f (exist _ n (le_n (S n)))). abstract lia.
  + destruct n.
    - intros [f [g [H H0]]]. destruct (g (exist _ m (le_n (S m)))). abstract lia.
    - intros. f_equal. apply IHm. apply (bijection_between_fins_aux H).
Qed.

view this post on Zulip zaa (Apr 20 2022 at 22:44):

Now I can sleep peacefully. Will buy myself an ice-cream tomorrow, probably.

view this post on Zulip Notification Bot (Apr 21 2022 at 04:14):

zaa has marked this topic as resolved.

view this post on Zulip Gaëtan Gilbert (Apr 21 2022 at 09:52):

Proof of (option A <~> option B) -> A <~> B if anyone needs one

Definition option_get {A} (o:option A) (H:o <> None) : A.
Proof.
  destruct o;auto.
  exfalso. apply H;reflexivity.
Defined.

Lemma option_get_ok {A} (x:A) o (H:o=Some x) H' : option_get o H' = x.
Proof.
  unfold option_get.
  destruct o;congruence.
Qed.

Lemma option_get_carac {A} o H : o = Some (@option_get A o H).
Proof.
  unfold option_get.
  destruct o;congruence.
Qed.

Module IsMap.
  Section S.

    Context {A B} (f:option A -> option B) g (Hfg:forall y, f (g y) = y) (Hgf:forall x, g (f x) = x).

    Hypothesis fNone : f None = None.

    Lemma gNone : g None = None.
    Proof.
      congruence.
    Qed.

    Lemma fSome x : f (Some x) <> None.
    Proof.
      congruence.
    Qed.

    Lemma gSome y : g (Some y) <> None.
    Proof.
      congruence.
    Qed.

    Definition F (x:A) : B := option_get _ (fSome x).
    (* this produces
match f (Some x) as o return (o <> None -> B) with
       | Some a => fun _ : Some a <> None => a
       | None => fun H : None <> None => False_rect B (H eq_refl)
       end (fSome x)

we may be tempted instead to do
match f (Some x) as o return (f (Some x) = o -> B) with
       | Some a => fun _ : f (Some x) = Some a => a
       | None => fun H : f (Some x) = None => False_rect B (fSome H)
       end eq_refl

however I cannnot find a way to prove anything about the later for abstract f
(trying to destruct (f (Some x)) while that match appears in the goal fails)
*)

    Definition G (y:B) : A := option_get _ (gSome y).

    Lemma F_carac x y (H:f (Some x) = Some y) : F x = y.
    Proof.
      unfold F.
      apply option_get_ok.
      exact H.
    Qed.

    Lemma G_carac y x (H:g (Some y) = Some x) : G y = x.
    Proof.
      unfold G.
      apply option_get_ok.
      exact H.
    Qed.

    Lemma FG y : F (G y) = y.
    Proof.
      destruct (g (Some y)) as [x|] eqn:Hgy;try congruence.
      destruct (f (Some x)) as [y'|] eqn:Hfx;try congruence.
      rewrite (G_carac _ _ Hgy),(F_carac _ _ Hfx).
      congruence.
    Qed.

    Lemma GF x : G (F x) = x.
    Proof.
      destruct (f (Some x)) as [y|] eqn:Hfx;try congruence.
      destruct (g (Some y)) as [x'|] eqn:Hgy;try congruence.
      rewrite (F_carac _ _ Hfx),(G_carac _ _ Hgy).
      congruence.
    Qed.

    Lemma f_carac x : f x = option_map F x.
    Proof.
      destruct x as [x|];simpl;auto.
      destruct (f (Some x)) as [y|] eqn:Hfx;try congruence.
      f_equal;symmetry.
      apply F_carac;assumption.
    Qed.

    Lemma g_carac y : g y = option_map G y.
    Proof.
      destruct y as [y|];simpl;try apply gNone.
      destruct (g (Some y)) as [x|] eqn:Hgy;try congruence.
      f_equal;symmetry.
      apply G_carac;assumption.
    Qed.

  End S.
End IsMap.

Module IsSwap.
  Section S.
    Context {A B} (f:option A -> option B) g (Hfg:forall y, f (g y) = y) (Hgf:forall x, g (f x) = x).

    Hypothesis (fNone:f None <> None).

    Definition yNone := option_get _ fNone.

    Lemma gNone : g None <> None.
    Proof.
      congruence.
    Qed.

    Definition xNone := option_get _ gNone.

    Definition F (x:A) : B :=
      match f (Some x) with
      | Some y => y
      | None => yNone
      end.

    Definition G (y:B) : A :=
      match g (Some y) with
      | Some x => x
      | None => xNone
      end.

    Lemma f_xNone : f (Some xNone) = None.
    Proof.
      unfold xNone.
      rewrite <-option_get_carac;congruence.
    Qed.

    Lemma g_yNone : g (Some yNone) = None.
    Proof.
      unfold yNone.
      rewrite <-option_get_carac;congruence.
    Qed.

    Lemma F_xNone : F xNone = yNone.
    Proof.
      unfold F.
      rewrite f_xNone.
      reflexivity.
    Qed.

    Lemma G_yNone : G yNone = xNone.
    Proof.
      unfold G.
      rewrite g_yNone.
      reflexivity.
    Qed.

    Lemma FG y : F (G y) = y.
    Proof.
      unfold G.
      destruct (g (Some y)) as [x|] eqn:Hgy.
      - unfold F.
        destruct (f (Some x)) as [y'|] eqn:Hfx;congruence.
      - rewrite F_xNone.
        pose proof (option_get_carac _ fNone).
        unfold yNone. congruence.
    Qed.

    Lemma GF x : G (F x) = x.
    Proof.
      unfold F.
      destruct (f (Some x)) as [y|] eqn:Hfx.
      - unfold G.
        destruct (g (Some y)) as [x'|] eqn:Hgy;congruence.
      - rewrite G_yNone.
        pose proof (option_get_carac _ gNone).
        unfold xNone. congruence.
    Qed.
  End S.
End IsSwap.

Section S.
  Context {A B} (f:option A -> option B) g (Hfg:forall y, f (g y) = y) (Hgf:forall x, g (f x) = x).

  Definition fNone : {f None = None} + {f None <> None}.
  Proof.
    destruct (f None);constructor;congruence.
  Defined.

  Definition F := match fNone with left H => IsMap.F f g Hgf H | right H => IsSwap.F f H end.

  Definition G := match fNone with left H => IsMap.G f g Hfg H | right H => IsSwap.G f g Hfg H end.

  Lemma FG y : F (G y) = y.
  Proof.
    unfold F,G;destruct fNone.
    - apply IsMap.FG.
    - apply IsSwap.FG.
  Qed.

  Lemma GF x : G (F x) = x.
  Proof.
    unfold F,G;destruct fNone.
    - apply IsMap.GF.
    - apply IsSwap.GF.
      (* Hgf doesn't appear in the goal but is needed by IsSwap.GF
         (because IsSwap.F and G have asymetric variable usage) *)
      exact Hgf.
  Qed.
End S.

Last updated: Sep 23 2023 at 07:01 UTC