## Tuesday, 2 December 2008

### Axiom Free NoConfusion in Coq

`Require Import Cast.Require Import Fin.Ltac prove_noConfusion :=  intros;    match goal with Eql : ?x = _ |- _ =>      elim Eql; elim x; simpl; tauto end.(*Inductive nat : Set :=| O : nat| S : nat -> nat.*)Definition NoConfusion_nat (P : Type) (x y : nat) : Type :=  match x, y with    | O, O => P -> P    | O, S y => P    | S x, O => P    | S x, S y => (x = y -> P) -> P  end.Definition noConfusion_nat (P : Type) (x y : nat) :  x = y -> NoConfusion_nat P x y.prove_noConfusion.Defined.Definition eq_nat_dec : forall x y : nat, {x = y} + {x <> y}.decide equality.Defined.Definition eq_nat_dec' : forall x y : nat, x = y \/ x <> y.decide equality.Defined.(*Inductive Fin : nat -> Set :=| fz : forall n, Fin (S n)| fs : forall n, Fin n -> Fin (S n).*)Notation FinINeq f g := (INeq nat Fin _ f _ g).Definition NoConfusion_Fin (P : Type) (i : nat) (x y : Fin i) : Type :=  match x, y with    | fz _, fz _ => P -> P    | fz _, fs _ _ => P    | fs _ _, fz _=> P    | fs x_i x, fs y_i y => (FinINeq x y -> P) -> P  end.Definition noConfusion_Fin (P : Type) (i : nat) (x y : Fin i) :  x = y -> NoConfusion_Fin P i x y.prove_noConfusion.Defined.Definition fz_fs_clash (P : Type) (n : nat) (f : Fin n)  : fz = fs f -> P  := fun Eq =>    noConfusion_Fin P (S n) (fz) (fs f) Eq.Definition fs_inj {n} {f f' : Fin n}  : fs f = fs f' -> f = f'  := fun Eq =>    noConfusion_Fin (f = f') _ _ _ Eq (INeq_eq nat Fin eq_nat_dec _ _ _).Inductive type : Set :=| Nat : type| Arrow : type -> type -> type.Definition eq_type_dec (s t : type) : { s = t } + { s <> t }.decide equality.Defined.Section equand.Variable vars : nat.Inductive equand : type -> Set :=| Zero : equand Nat| Succ : equand (Arrow Nat Nat)| VAR (V : Fin vars) : equand Nat| APP {A B} : equand (Arrow A B) -> equand A -> equand B.Notation equandINeq f g := (INeq type equand _ f _ g).Definition NoConfusion_equand (P : Type) (i : type) (x y : equand i) : Type :=  match x, y with    | Zero, Zero => P -> P    | Succ, Succ => P -> P    | VAR f, VAR f' => (f = f' -> P) -> P    | APP xi xj xf xo, APP yi yj yf yo =>      (equandINeq xf yf -> equandINeq xo yo -> P) -> P    | _, _ => P  end.Definition noConfusion_equand (P : Type) (i : type) (x y : equand i) : x = y -> NoConfusion_equand P i x y.prove_noConfusion.Defined.Definition Zero_One_clash (P : Type) (i : type)  : Zero = APP Succ Zero -> P  := fun Eq =>    noConfusion_equand P Nat Zero (APP Succ Zero) Eq.Definition APP_f_inj (u v : type) (F F' : equand (Arrow u v)) (O O' : equand u)  : @APP u v F O = @APP u v F' O' -> F = F'  := fun Eq =>    noConfusion_equand (F = F') _ _ _ Eq    (fun FEq OEq => INeq_eq _ _ eq_type_dec _ _ _ FEq).Definition APP_o_inj (u v : type) (F F' : equand (Arrow u v)) (O O' : equand u)  : @APP u v F O = @APP u v F' O' -> O = O'  := fun Eq =>    noConfusion_equand (O = O') _ _ _ Eq    (fun FEq OEq => INeq_eq _ _ eq_type_dec _ _ _ OEq).Definition eq_equand_dec : forall (t : type)(u v : equand t), {u = v} + {u <> v}.apply INeq_dec_dec.apply eq_type_dec.refine (fix eq_equand_dec (i : type) (I : equand i)                          (i' : type) (I' : equand i') {struct I} :                          {@INeq _ _ i I i' I'} + {~ @INeq _ _ i I i' I'} := _).refine (match I as I in equand i, I' as I' in equand i'        return {@INeq _ _ i I i' I'} + {~ @INeq _ _ i I i' I'}        with          | Zero, Zero => _          | Zero, Succ => _          | Zero, VAR _ => _          | Zero, APP _ _ _ _ => _          | Succ, Zero => _          | Succ, Succ => _          | Succ, VAR _ => _          | Succ, APP _ _ _ _ => _          | VAR _, Zero => _          | VAR _, Succ => _          | VAR _, VAR _ => _          | VAR _, APP _ _ _ _ => _          | APP _ _ _ _, Zero => _          | APP _ _ _ _, Succ => _          | APP _ _ _ _, VAR _ => _          | APP _ _ _ _, APP _ _ _ _ => _        end);try solve [ discriminate          | left; reflexivity          | right; intro Q; inversion Q          | destruct B; right; intro Q; inversion Q; discriminate          ].destruct (fin_eq_dec V V0); subst.left; reflexivity.right; intro Q; inversion Q; contradiction.destruct (eq_type_dec B B0);(destruct (eq_equand_dec _ e0 _ e2) as [Q|N];[inversion Q|idtac]);(destruct (eq_equand_dec _ e _ e1) as [Q'|N'];[inversion Q'|idtac]);  subst;try solve [ left;  rewrite Q; try apply eq_type_dec;  rewrite Q'; try apply eq_type_dec;    reflexivity ];right; intro NQ;  try inversion NQ;  try inversion Q;  try inversion Q';  try contradiction;  try subst;  try pose (APP_f_inj _ _ _ _ _ _ (INeq_eq _ _ eq_type_dec _ _ _ NQ));  try pose (APP_o_inj _ _ _ _ _ _ (INeq_eq _ _ eq_type_dec _ _ _ NQ)).apply N'; rewrite e3; reflexivity.apply N; rewrite e4; reflexivity.apply N; rewrite e4; reflexivity.Defined.Eval compute in (eq_equand_dec _  (APP Succ (APP Succ Zero))  (APP Succ (APP Succ Zero))).End equand.Print Assumptions eq_equand_dec.(* *  = left (APP Succ (APP Succ Zero) = APP Succ (APP Succ Zero) -> False) *      (refl_equal (APP Succ (APP Succ Zero))) *  : {APP Succ (APP Succ Zero) = APP Succ (APP Succ Zero)} + *    {APP Succ (APP Succ Zero) <> APP Succ (APP Succ Zero)} * * Computed fully, no JMeq_eq axiom stopping reduction * *)Require Import Coven.Require Import Arith.Require Import Omega.Print le.Lemma le_irrelevent : forall n m (H1 H2:le n m), H1=H2.refine (fix le_irrelevent n m (H1 H2:le n m) {struct H1} : H1=H2 := _).apply INeq_eq; auto with arith.refine (  match H1 as H1' in _ <= m', H2 as H2' in _ <= m''  return m = m' ->         m = m'' ->         INeq nat (le n) m H1 m' H1' ->         INeq nat (le n) m H2 m'' H2' ->         INeq nat (le n) m H1 m H2  with    | le_n, le_n => fun m'eq m''eq H1eq H2eq => _    | le_n, le_S p_m p_le => fun m'eq m''eq H1eq H2eq => !    | le_S p_m p_le, le_n => fun m'eq m''eq H1eq H2eq => !    | le_S p_m p_le, le_S p_m' p_le' => fun m'eq m''eq H1eq H2eq => _  end  (refl_equal _)  (refl_equal _)  (INeq_refl _ _ _ _)  (INeq_refl _ _ _ _)); subst; subst.rewrite (INeq_eq _ _ eq_nat_dec _ _ _ H1eq).rewrite (INeq_eq _ _ eq_nat_dec _ _ _ H2eq).reflexivity.omega.omega.injection m''eq; intro; subst.rewrite (INeq_eq _ _ eq_nat_dec _ _ _ H1eq).rewrite (INeq_eq _ _ eq_nat_dec _ _ _ H2eq).rewrite (le_irrelevent _ _ p_le p_le').reflexivity.Qed.Print Assumptions le_irrelevent.(** Closed under the global context **)`