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 **)

No comments: