CoqUIP

dumb.v

Require Import PeanoNat.
Require Import Coq.Logic.Eqdep_dec. 
Import EqNotations.
Require Import Coq.Logic.JMeq.


Infix "==" := JMeq (at level 70, no associativity).

Print JMeq.
Print eq.

Inductive T (n : nat) : Type := foo.

Definition cast1 {n : nat} (t : T n) : T (n + 0) :=
  rew (plus_n_O n) in t.

Definition cast2 {n i : nat} (t : T (S n + i)) : T (n + S i) :=
  rew (Nat.add_succ_comm n i) in t.

Definition cast3 {n : nat} (t : T (S n)) : T (n + 1) :=
  rew (eq_sym (Nat.add_1_r n)) in t.


Lemma eq_rew {n m : nat} (t : T n) (p q : n = m) : rew p in t = rew q in t.
Proof.
    (* 
    rew is parameterized by an equality. Show that these equalities are equal.

    that is, show p = q where
    p : n = m
    and
    q : n = m

    by using UIP_dec and the fact that nat has decidable equality
  
    UIP_dec
     : forall A : Type, (forall x y : A, {x = y} + {x <> y}) -> forall (x y : A) (p1 p2 : x = y), p1 = p2
    
*)
  assert (p = q).
  - rewrite (UIP_dec Nat.eq_dec p q). reflexivity.
  - subst. reflexivity.
Qed.

Lemma eq_cast {n : nat} (t : T (S n)) : cast2 (cast1 t) = cast3 t.
Proof.
  unfold cast1, cast2, cast3.
  rewrite rew_compose.   (* turn the nested `rew` into a single rew *)
  apply eq_rew.
Qed.


Definition next {n : nat} (t : T n) : T (S n) := foo _.

Lemma annoying {n : nat}(t : T (1 + n))(s : T (n + 1)) : s == t.
Proof.
  destruct s. destruct t.
  rewrite Nat.add_1_r. reflexivity.
Qed.
Print annoying.

(*
 From Equations Require Import Equations.
Equations fromjmeq (a b : nat) (p : a == b) : a = b := 
fromjmeq _ _ JMeq_refl := eq_refl.
*)


Lemma huh { n m : nat} : n = m -> T n = T m.
Proof.
  intros.
  congruence.
Qed.

Require Import Program.Equality.

Lemma asdf (n : nat) (t : T n) (s : T (n + 0)) : cast1 t = s.
Proof.
  unfold cast1.
  destruct eq_rect.
  destruct s. reflexivity.
Qed.


Module KAxiom.
(* escape hatch to Agda like pattern matching *)
From Equations Require Import Equations.
Set Equations With UIP.

Axiom UIP_Type : UIP Type.
Local Existing Instance UIP_Type.


(*
https://github.com/agda/agda-stdlib/blob/1798dfce3d2aeb0e0acbddaaba029cc61dc5a31e/src/Relation/Binary/HeterogeneousEquality.agda#L107
*)
Equations icong {I : Type}{A : I -> Set}{B : forall {k : I}, A k -> Set} 
                 {i j : I}{x : A i} {y : A j}( p : i = j)(f : forall {k : I}(z : A k), B z) : x ~= y -> f _ x ~= f _  y:=
icong eq_refl _ JMeq_refl := JMeq_refl.
 

Lemma fk {n m : nat} (s : T n) (t : T m)(p : n  = m): s == t -> next s == next t.
Proof.
  intros.
  apply (@icong nat T (fun k _ => T (S k)) n m s t p (fun k => @next k) H).
Qed.

  









Print eq_ind_r.


Print JMeq.


Definition tojmeq (A : Type) (a b : A) (p : a = b) : a == b :=
  match p with
   | eq_refl => JMeq_refl 
  end.


Definition Vec (A : Type ): nat -> Type :=
  fix vec n := match n return Type with
               | O   => unit
               | S n => prod A (vec n)
               end.

Compute (Vec bool 3).


Lemma wtf {n : nat} (A : Type) (s : Vec A (S n)) (t : Vec A (n + 1)) : s = t.



Definition bar : Vec bool 3 := (true,(false, (true, tt))).

Equations fromjmeq (A : Type) (a b : A) (p : a == b) : a = b := 
fromjmeq _ _ _ JMeq_refl := eq_refl.

Definition fromjmeq (A : Type) (a b : A) (p : a == b) : a = b :=
  match p with
   | JMeq_refl => eq_refl 
  end.
Equations tojmeq (A : Type) (a b : A) (p : a = b) : a == b := 
tojmeq _ _ _ eq_refl := JMeq_refl.