Tmp.v

Require Import Lia
  Coq.Unicode.Utf8
  Coq.Bool.Bool 
  Coq.Init.Byte
  Coq.NArith.NArith
  Coq.Strings.Byte
  Coq.ZArith.ZArith
  Coq.Lists.List.
  
Import Notations ListNotations.
Local Open Scope N_scope.

Definition np_total (np : N) :  (np <? 256 = true) ->  byte.
Proof.
  intros H.
  refine(match (np <? 256) as b return ∀ mp, np = mp -> 
      (mp <? 256) = b -> _ with 
   | true => fun mp Hmp Hmpt => 
      match of_N mp as npt return _ = npt -> _ with 
      | Some x => fun _ => x
      | None => fun Hf => _  
      end eq_refl
   | false => fun mp Hmp Hmf => _
  end np eq_refl eq_refl).
  abstract(
  apply of_N_None_iff in Hf;
  apply N.ltb_lt in Hmpt; nia).
  abstract (subst; congruence).
Defined.

Lemma np_true : forall np (H : np <? 256 = true) x, 
  of_N np = Some x -> np_total np H = x.
Proof.
  intros * Ha. unfold np_total.
  case_eq (np <? 256); intro Hb.
  generalize (np_total_subproof np np eq_refl Hb) as Hc.
  rewrite Ha.
  intros. reflexivity.
  pose proof (eq_trans (eq_sym H) Hb).
  congruence.
  Show Proof.
Qed.
 

Definition a := O.

Theorem a_is_zero : a = O.
Proof.
  reflexivity.
Qed.

Import EqNotations.
Lemma ex_intro_gen : forall (P : nat -> Prop) (x y : nat) 
  (Ha : x = y) (Hb : P x),
  ex_intro P x Hb = ex_intro P y (eq_rect x P Hb y Ha).
Proof.
  intros *; subst;
  cbn; exact eq_refl.
Qed.


Theorem test : forall (P : nat -> Prop) (Ha : P O),
  ex_intro P O Ha = ex_intro P a Ha.
Proof.
  intros *.
  Fail eapply ex_intro_gen.
  Fail rewrite a_is_zero.
  (* 
    Reason is: Illegal application: 
    The term "ex_intro" of type
    "∀ (A : Type) (P : A → Prop) (x : A), P x → ∃ y, P y"

    So let's generalize this.
  *)
  generalize (ex_intro _ a a_is_zero).
  intros (y & Hb).
  generalize (@eq_refl _ a).
  generalize a at 1.
  (* if I change to -1, it does not work *)
  intros ? Hc.
  rewrite (eq_trans Hb Hc).


  rewrite <-Hc.
  (* I am chasing my tail ?? *)