Failcommented.v

From Stdlib Require Import Utf8 Fin Psatz List.

Definition cardinality (n : nat) (A : Type) : Prop :=
  exists (f : A -> Fin.t n) (g : Fin.t n -> A),
    (forall x, g (f x) = x) ∧ (forall y, f (g y) = y).


Definition bool_to_Fin_2 (x : bool) : Fin.t 2 :=
  if x then Fin.FS Fin.F1 else Fin.F1.


Definition Fin_2_to_bool (y : Fin.t 2) : bool :=
  match y with
    | F1 => false
    | FS F1 => true
    | _ => false (* bogus! *)
  end.

Theorem bool_cardinality_2 :
  cardinality 2 bool.
Proof.
  unfold cardinality.
  exists bool_to_Fin_2.
  exists Fin_2_to_bool.
  split.
  +
    destruct x; cbn; reflexivity.
  +
    intro y. 
    refine
    (match y as y' in Fin.t n' 
      return 
        forall (pf : n' = 2), 
        (match n' return Fin.t n' -> Type 
        with 
        | 2 => fun (eb : Fin.t 2) => 
          match eb as eb' in Fin.t n'' return n'' = 2 -> Fin.t n'' -> Type 
          with 
          | _ => fun pfa eb' => 
            (bool_to_Fin_2 (Fin_2_to_bool (eq_rect _ Fin.t eb' 2 pfa))) = 
              (eq_rect _ Fin.t eb' 2 pfa)
          end eq_refl eb
        | _ => fun _ => IDProp 
        end y')
    with 
    | F1 => _ 
    | FS f => 
      match f with 
      | F1 => _ 
      | FS _ => _ 
      end
    end eq_refl).
    ++
      intros ha.
      assert (n = 1). nia.
      subst. exact eq_refl.
    ++
      intro ha.
      assert (n0 = 0). nia.
      subst. reflexivity.
    ++
      intro ha.
      assert (n0 = 0). nia.
      subst. cbn. 
      refine match t with end.
Qed.


(* 

Inductive t : nat -> Set :=
| t_S : forall (n : nat), t (S n).

Goal forall (n : nat) (p : t (S n)), p = t_S n.
Proof.
  intros n p.
  refine
  (match p as p' in t n' return 
    (match n' return t n' -> Prop 
    with 
    | 0 => fun _ => IDProp
    | S n'' => fun (ea : t (S n'')) => ea = t_S n'' 
    end p')
  with 
  | t_S n' => eq_refl
  end).
Qed. 


Program Definition nth_safe {A} (l: list A) (n: nat) 
  (IN: (n < length l)%nat) : A :=
  match (nth_error l n) with
    | Some res => res
    | None => _
  end.
Next Obligation.
  symmetry in Heq_anonymous. apply nth_error_None in Heq_anonymous. lia.
Defined.

Lemma nth_safe_nth: forall A (l: list A) (n: nat) d (IN: (n < length l)%nat), nth_safe l n IN = nth n l d.
Proof.
  intros A l n d IN.
  unfold nth_safe.
  set (x := nth_safe_obligation_1 _ _ _ _); clearbody x; cbn in x.
  destruct nth_error eqn:Heq.
  - symmetry.
    now apply nth_error_nth.
  - apply nth_error_None in Heq.
    lia.
Qed.


Lemma nth_safe_nthth : forall A (l: list A) (n: nat) d (IN: (n < length l)%nat), nth_safe l n IN = nth n l d.  
Proof.
  intros A l n d IN. unfold nth_safe. 
  generalize (eq_refl (nth_error l n)) as e.
  generalize (nth_error l n) at 1 3.
  intros *. destruct o as [o' |].
  +
    symmetry.
    now apply nth_error_nth.
  +
    pose proof (proj1 (@nth_error_None _ _ _) (eq_sym e)).
    nia.
Qed.



Inductive Nat : Type := 
| O : Nat 
| S : Nat -> Nat.

Theorem nat_inv :  O <> S O.
Proof.
  intro ha. inversion ha. Show Proof.
  refine
  (match ha as ha' in _ = e return 
    e = S O -> False
  with
  | eq_refl => _ 
  end eq_refl). Check False_rect.

From Coq Require Import Init.Prelude Unicode.Utf8.
From mathcomp Require Import all_ssreflect.

Require Import Coq.Logic.Classical.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.


Lemma oStar_perm_choiceTT : 
  forall (T : finType) (u : {set T}) (o : T) (o2 : {o | o \in u}) (ot : o \in u),
  o = sval ((if o \in u as y return ((o \in u) = y → {o : T | o \in u})
             then [eta exist (λ o : T, o \in u) o]
             else fun=> o2)
              (erefl (o \in u))).
Proof.
  move=> T u o.
  case=> o2 p ou.
  have foo : o = sval (exist (fun o => o \in u) o ou) by [].
  rewrite [LHS]foo.
  apply/eq_sig_hprop_iff => /=; first by move=> x; 
  apply: Classical_Prop.proof_irrelevance.
  (* move: erefl; rewrite {2 3}ou => ou'; congr exist.  exact: bool_irrelevance. *)
  (* 
  generalize (erefl (o \in u)).
  generalize ((o \in u)) at 2 3.
  intros *. destruct b; 
  [eapply f_equal, Classical_Prop.proof_irrelevance | 
  congruence]. *)

  set (fn := fun (ofn1 ofn2 : T) (ufn : {set T}) (pfa : ofn1 \in ufn) 
    (pfb : ofn2 \in ufn) (b : bool) 
    (pfc : (ofn1 \in ufn) = b) => 
    (if b as y return ((ofn1  \in ufn) = y → {o0 : T | o0  \in ufn})
    then [eta exist (λ o0 : T, o0  \in ufn) ofn1]
    else fun=> exist (λ o0 : T, o0  \in ufn) ofn2 pfb) pfc).
  enough (forall (ofn1 ofn2 : T) (ufn : {set T}) pfa pfb b pfc,
    exist (λ o0 : T, o0  \in ufn) ofn1 pfa = 
    fn ofn1 ofn2 ufn pfa pfb b pfc) as ha.
  eapply ha.
  intros *.
  destruct b; cbn.
  f_equal.
  eapply Classical_Prop.proof_irrelevance.
  congruence.
Qed.

  


From Stdlib Require Import Utf8 Psatz Arith.


Section UIP.


  (* n <= m *)
  Fixpoint le_bool (n m : nat) : bool := 
    match n as n' in nat return bool 
    with 
    | 0 => true 
    | S n' => match m as m' in nat return bool 
      with 
      | 0 => false 
      | S m' => le_bool n' m' 
      end 
    end.

  Theorem le_bool_prop : ∀ (n m : nat), 
    reflect (le n m) (le_bool n m).
  Proof.
    induction n as [|n ihn].
    +
      cbn; constructor.
      nia.
    +
      destruct m as [|m'].
      ++
        cbn; constructor.
        nia.
      ++
        cbn. specialize (ihn m').
        destruct ((le_bool n m'));
        constructor; inversion ihn; nia.
  Defined.
  
  Theorem le_unique_reflection : ∀ (n m : nat) (ha hb : le n m),
    ha = hb.
  Proof.
    intros n m.
    Print Bool.iff_reflect.
    rewrite le_bool_prop.
   


  (* Set Printing Implicit. *)
  Theorem uip_nat : ∀ (n : nat) (pf : n = n), pf = @eq_refl nat n.
  Proof.
    refine(fix fn (n : nat) : ∀ (pf : n = n), pf = @eq_refl nat n := 
      match n as n' in nat return 
        ∀ (pf : n' = n'), pf = @eq_refl nat n' 
      with 
      | 0 => fun pf => _ 
      | S np => fun pf => _ 
      end). 
    +
      refine
        (match pf as pf' in _ = n' return 
          (match n' as n'' return 0 = n'' -> Type 
          with 
          | 0 => fun (e : 0 = 0) => e = @eq_refl _ 0 
          | S n' => fun _ => IDProp 
          end pf')
        with 
        | eq_refl => eq_refl
        end).
      +
        specialize (fn np (f_equal Nat.pred pf)).
        change eq_refl with (f_equal S (@eq_refl _ np)).
        rewrite <-fn; clear fn.
        refine 
        (match pf as pf' in _ = n' return 
          (match n' as n'' return S np = n'' -> Type 
          with 
          | 0 => fun _ => IDProp
          | S n'' => fun e => e = f_equal S (f_equal Nat.pred e)
          end pf')
        with 
        | eq_refl => eq_refl
        end).
  Defined.




  Scheme le_dep_ind := Induction for le Sort Prop.
  Theorem le_unique_ind : ∀ (n m : nat) (ha hb : le n m), ha = hb.
  Proof.
    induction ha using le_dep_ind.
    +
      refine(fun hc =>
        match hc as hc' in _ ≤ n' return ∀ (pfb : n = n'),
          le_n n' = @eq_rect _ n (fun w => w ≤ n') hc' n' pfb
        with
        | le_n _ => _
        | le_S _ nw pfb => _
        end eq_refl).
      ++
        intros *.
        pose proof (uip_nat n pfb) as ha.
        rewrite ha. exact eq_refl.
      ++
        intros pfc.
        nia.
    +
      refine(fun hb =>
        match hb as hb' in _ ≤ mp return ∀ (pf : mp = S m),
          le_S n m ha = @eq_rect _ mp (fun w => n <= w) hb' (S m) pf 
        with
        | le_n _ => _
        | le_S _ nw pfc => _
        end eq_refl).
      ++
        intros *.
        nia.
      ++
        intros *.
        inversion pf as [pf']; subst.
        pose proof (uip_nat _ pf) as hc.
        rewrite hc. cbn. 
        erewrite IHha. eapply f_equal.
        exact eq_refl.
  Defined.

  Lemma nat_lt_irr n m (p q : n < m) : p = q.
  Proof.
    eapply le_unique_ind.
  Qed.




  Theorem le_unique_fail : ∀ (n m : nat) (ha hb : le n m), ha = hb.
  Proof.
    refine(fix fn (n m : nat) (ha : le n m) {struct ha} : 
      ∀ (hb : le n m), ha = hb := 
      match ha as ha' in le _ m' return ∀(pfa : m = m'), 
        ha = @eq_rect nat m' (fun w => le n w) ha' m (eq_sym pfa) -> 
        ∀ (hb : le n m'), ha' = hb 
      with
      | le_n _ =>  _ 
      | le_S _ m' pfb => _ 
      end eq_refl eq_refl).
    +
      intros * hb hc.
      generalize dependent hc.
      refine(fun hc => 
        match hc as hc' in _ ≤ n' return ∀ (pfb : n = n'), 
          le_n n' = @eq_rect _ n (fun w => w ≤ n') hc' n' pfb  
        with 
        | le_n _ => _ 
        | le_S _ nw pfb => _ 
        end eq_refl).     
        ++
          intros *. 
          assert (hd : pfb = eq_refl) by 
          (apply uip_nat).
          subst; cbn; exact eq_refl. 
        ++
          intros pfc. subst.
          abstract nia.  
    +
      intros * hb hc.
      generalize dependent pfb.
      generalize dependent pfa.
      generalize dependent hc.
      refine(fun hc => 
        match hc as hc' in _ ≤ (S mp) return ∀ (pf : mp = m') pfa pfb hb,
          le_S n mp (@eq_rect _ m' (fun w => n ≤ w) pfb mp (eq_sym pf)) = hc'
        with 
        | le_n _ => _ 
        | le_S _ nw pfc => _
        end eq_refl).
      ++
        destruct n as [| n].
        +++ exact idProp.
        +++
          intros * hb. abstract nia.
      ++
        intros * hb. subst; cbn.
        f_equal. eapply fn. 
        Fail Guarded.
  Admitted.
  
    

  Theorem le_unique : ∀ (n m : nat) (ha hb : le n m), ha = hb.
  Proof.
    refine(fix fn (n m : nat) (ha : le n m) {struct ha} : 
      ∀ (hb : le n m), ha = hb := 
      match ha as ha' in le _ m' return ∀(pfa : m = m'), 
        ha = @eq_rect nat m' (fun w => le n w) ha' m (eq_sym pfa) -> 
        ∀ (hb : le n m'), ha' = hb 
      with
      | le_n _ =>  _ 
      | le_S _ m' pfb => _ 
      end eq_refl eq_refl).
    +
      intros * hb hc.
      generalize dependent hc.
      refine(fun hc => 
        match hc as hc' in _ ≤ n' return ∀ (pfb : n = n'), 
          le_n n' = @eq_rect _ n (fun w => w ≤ n') hc' n' pfb  
        with 
        | le_n _ => _ 
        | le_S _ nw pfb => _ 
        end eq_refl).     
        ++
          intros *. 
          assert (hd : pfb = eq_refl) by 
          (apply uip_nat).
          subst; cbn; exact eq_refl. 
        ++
          intros pfc. subst.
          abstract nia.  
    +
      intros * hb hc. 
      generalize dependent pfb.
      generalize dependent pfa.
      generalize dependent hc.
      refine(fun hc => 
        match hc as hc' in _ ≤ mp return ∀ (pf : mp = S m') pfa pfb hb,
          le_S n m' pfb = @eq_rect _ mp _ hc' (S m') pf   
        with 
        | le_n _ => _ 
        | le_S _ nw pfc => _
        end eq_refl).
      ++
        intros * hb. subst. 
        abstract nia.
      ++
        intros * hb.   
        inversion pf as [hpf]; subst.
        assert (hd : pf = eq_refl) by 
        (apply uip_nat). 
        subst; cbn. 
        f_equal; eapply fn.
  Defined.


  Theorem le_unique_didnot_fail : ∀ (n m : nat) (ha hb : le n m), ha = hb.
  Proof.
    refine(fix fn (n m : nat) (ha : le n m) {struct ha} : 
      ∀ (hb : le n m), ha = hb := 
      match ha as ha' in le _ m' return ∀(pfa : m = m'), 
        ha = @eq_rect nat m' (fun w => le n w) ha' m (eq_sym pfa) -> 
        ∀ (hb : le n m'), ha' = hb 
      with
      | le_n _ =>  _ 
      | le_S _ m' pfb => _ 
      end eq_refl eq_refl).
    +
      intros * hb hc.
      refine(match hc as hc' in _ ≤ n' return ∀ (pfb : n = n'), 
          le_n n' = @eq_rect _ n (fun w => w ≤ n') hc' n' pfb  
        with 
        | le_n _ => _ 
        | le_S _ nw pfb => _ 
        end eq_refl).     
        ++
          intros *. 
          assert (hd : pfb = eq_refl) by 
          (apply uip_nat).
          subst; cbn; exact eq_refl. 
        ++
          intros pfc. subst.
          abstract nia.  
    +
      intros * hb hc.
      refine(match hc as hc' in _ ≤ (S mp) return ∀ (pf : mp = m'),
          le_S n mp (@eq_rect _ m' (fun w => n ≤ w) pfb mp (eq_sym pf)) = hc'
        with 
        | le_n _ => _ 
        | le_S _ nw pfc => _
        end eq_refl).
      ++
        destruct n as [| n].
        +++ exact idProp.
        +++
          intros *. abstract nia.
      ++
        intros *. subst; cbn.
        f_equal. eapply fn.
  Defined.
  

  (* this one works *)
  Theorem le_unique_fn_earlier : ∀ (n m : nat) (ha hb : le n m), ha = hb.
  Proof.
    refine(fix fn (n m : nat) (ha : le n m) {struct ha} :
      ∀ (hb : le n m), ha = hb :=
      match ha as ha' in le _ m' return ∀(pfa : m = m'),
        ha = @eq_rect nat m' (fun w => le n w) ha' m (eq_sym pfa) ->
        ∀ (hb : le n m'), ha' = hb
      with
      | le_n _ =>  _
      | le_S _ m' pfb => _
      end eq_refl eq_refl).
    +
      intros * hb hc.
      generalize dependent hc.
      refine(fun hc =>
        match hc as hc' in _ ≤ n' return ∀ (pfb : n = n'),
          le_n n' = @eq_rect _ n (fun w => w ≤ n') hc' n' pfb
        with
        | le_n _ => _
        | le_S _ nw pfb => _
        end eq_refl).
        ++
          intros *.
          assert (hd : pfb = eq_refl) by
          (apply uip_nat).
          subst; cbn; exact eq_refl.
        ++
          intros pfc. subst.
          abstract nia.
    + (* here we have pfb, the structurally smaller value *)
      specialize (fn _ _ pfb).
      Guarded.
      intros * hb hc.
      generalize dependent pfb.
      generalize dependent pfa.
      generalize dependent hc.
      refine(fun hc =>
        match hc as hc' in _ ≤ (S mp) return ∀ (pf : mp = m') pfa pfb fn hb,
          le_S n mp (@eq_rect _ m' (fun w => n ≤ w) pfb mp (eq_sym pf)) = hc'
        with
        | le_n _ => _
        | le_S _ nw pfc => _
        end eq_refl).
      ++
        destruct n as [| n].
        +++ exact idProp.
        +++
          intros * hb. abstract nia.
      ++
        intros * fn hb. subst; cbn.
        f_equal. eapply fn.
  Defined.

 
End UIP.
*)