Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
(* Cut elimination property for an entailment relation (sub) coming *) (* from a subtyping relation of BCD intersection types *) (* Olivier Laurent 06/12/04 *) Require Import Omega. Inductive formula : Set := var : nat -> formula | omega : formula | inter : formula -> formula -> formula | arrow : formula -> formula -> formula . Inductive sub : formula -> formula -> Prop := identity : forall a:formula, (sub a a) | omega_right : forall a:formula, (sub a omega) | inter_left1 : forall a b c:formula, (sub a b) -> (sub (inter a c) b) | inter_left2 : forall a b c:formula, (sub a b) -> (sub (inter c a) b) | inter_right : forall a b c:formula, (sub a b) -> (sub a c) -> (sub a (inter b c)) | arrow_right : forall a b c d e f:formula, (sub c (inter (arrow d e) (arrow d f))) -> (sub a d) -> (sub (inter e f) b) -> (sub c (arrow a b)) | omega_arrow : forall a b c:formula, (sub omega b) -> (sub c (arrow a b)) | arrow_var : forall c d e f:formula, forall x:nat, (sub c (inter (arrow d e) (arrow d f))) -> (sub omega d) -> (sub (inter e f) (var x)) -> (sub c (var x)) | var_arrow : forall a b:formula, forall x:nat, (sub (var x) b) -> (sub (var x) (arrow a b)) . Inductive sub_lg : formula -> formula -> nat -> Prop := identity_lg : forall a:formula, (sub_lg a a (S O)) | omega_right_lg : forall a:formula, (sub_lg a omega (S O)) | inter_left1_lg : forall a b c:formula, forall n:nat, (sub_lg a b n) -> (sub_lg (inter a c) b (S n)) | inter_left2_lg : forall a b c:formula, forall n:nat, (sub_lg a b n) -> (sub_lg (inter c a) b (S n)) | inter_right_lg : forall a b c:formula, forall n m:nat, (sub_lg a b n) -> (sub_lg a c m) -> (sub_lg a (inter b c) (S (n+m))) | arrow_right_lg : forall a b c d e f:formula, forall n m l:nat, (sub_lg c (inter (arrow d e) (arrow d f)) n) -> (sub_lg a d m) -> (sub_lg (inter e f) b l) -> (sub_lg c (arrow a b) (S (n+m+l))) | omega_arrow_lg : forall a b c:formula, forall n:nat, (sub_lg omega b n) -> (sub_lg c (arrow a b) (S n)) | arrow_var_lg : forall c d e f:formula, forall x:nat, forall n m l:nat, (sub_lg c (inter (arrow d e) (arrow d f)) n) -> (sub_lg omega d m) -> (sub_lg (inter e f) (var x) l) -> (sub_lg c (var x) (S (n+m+l))) | var_arrow_lg : forall a b:formula, forall x:nat, forall n:nat, (sub_lg (var x) b n) -> (sub_lg (var x) (arrow a b) (S n)) . Lemma exists_length : forall x y : formula, sub x y -> exists n : nat, sub_lg x y n. intros. induction H. exists (S O). apply identity_lg. exists (S O). apply omega_right_lg. inversion IHsub. exists (S x). apply inter_left1_lg ; assumption. inversion IHsub. exists (S x). apply inter_left2_lg ; assumption. inversion IHsub1. inversion IHsub2. exists (S (x + x0)). apply inter_right_lg ; assumption. inversion IHsub1. inversion IHsub2. inversion IHsub3. exists (S (x + x0 + x1)). apply (arrow_right_lg a b c d e f) ; assumption. inversion IHsub. exists (S x). apply omega_arrow_lg ; assumption. inversion IHsub1. inversion IHsub2. inversion IHsub3. exists (S (x0 + x1 +x2)). apply (arrow_var_lg c d e f x) ; assumption. inversion IHsub. exists (S x0). apply var_arrow_lg ; assumption. Qed. Lemma forget_length : forall x y : formula, forall n : nat, sub_lg x y n -> sub x y. intros. induction H. apply identity. apply omega_right. apply inter_left1 ; assumption. apply inter_left2 ; assumption. apply inter_right ; assumption. apply (arrow_right a b c d e f) ; assumption. apply omega_arrow ; assumption. apply (arrow_var c d e f x) ; assumption. apply var_arrow ; assumption. Qed. Lemma non_O_length : forall x y : formula, forall n : nat, sub_lg x y n -> ~ n = O. intros. inversion H; auto. Qed. Theorem sub_trans_length : forall k : nat, forall a b c : formula, forall n m : nat, (n+m <= k) -> (sub_lg a b n) -> (sub_lg b c m) -> (sub a c). intro. induction k ; intros. (* 0 length: impossible *) assert (~ n=O). apply (non_O_length a b n). assumption. elim H2. omega. (* true case *) inversion H1 ; subst b ; subst c. (* */identity *) apply (forget_length a a0 n) ; assumption. (* */omega *) apply omega_right. (* */inter_left1 *) inversion H0. (* identity/inter_left1 *) apply (forget_length (inter a0 c0) b0 m) ; assumption. (* inter_left1/inter_left1 *) apply inter_left1. apply (IHk a1 (inter a0 c0) b0 n1 m) ; try omega ; assumption. (* inter_left2/inter_left1 *) apply inter_left2. apply (IHk a1 (inter a0 c0) b0 n1 m) ; try omega ; assumption. (* inter_right/inter_left1 *) apply (IHk a a0 b0 n1 n0) ; try omega ; assumption. (* */inter_left2 *) inversion H0. (* identity/inter_left2 *) apply (forget_length (inter c0 a0) b0 m) ; assumption. (* inter_left1/inter_left2 *) apply inter_left1. apply (IHk a1 (inter c0 a0) b0 n1 m) ; try omega ; assumption. (* inter_left2/inter_left2 *) apply inter_left2. apply (IHk a1 (inter c0 a0) b0 n1 m) ; try omega ; assumption. (* inter_right/inter_left2 *) apply (IHk a a0 b0 m0 n0) ; try omega ; assumption. (* */inter_right *) apply inter_right. apply (IHk a a0 b0 n n0) ; try omega ; assumption. apply (IHk a a0 c0 n m0) ; try omega ; assumption. (* */arrow_right *) apply (arrow_right a0 b0 a d e f). apply (IHk a c0 (inter (arrow d e) (arrow d f)) n n0) ; try omega ; assumption. apply (forget_length a0 d m0) ; assumption. apply (forget_length (inter e f) b0 l) ; assumption. (* */omega_arrow *) apply omega_arrow. apply (forget_length omega b0 n0) ; assumption. (* */arrow_var *) apply (arrow_var a d e f x). apply (IHk a c0 (inter (arrow d e) (arrow d f)) n n0) ; try omega ; assumption. apply (forget_length omega d m0) ; assumption. apply (forget_length (inter e f) (var x) l) ; assumption. (* */var_arrow *) inversion H0. (* identity/var_arrow *) apply (forget_length (var x) (arrow a0 b0) m) ; assumption. (* inter_left1/var_arrow *) apply inter_left1. apply (IHk a1 (var x) (arrow a0 b0) n1 m) ; try omega ; assumption. (* inter_left2/var_arrow *) apply inter_left2. apply (IHk a1 (var x) (arrow a0 b0) n1 m) ; try omega ; assumption. (* arrow_var/var_arrow *) apply (arrow_right a0 b0 a d e f). apply (forget_length a (inter (arrow d e) (arrow d f)) n1) ; assumption. apply (IHk a0 omega d (S O) m0) ; try omega ; try assumption. apply omega_right_lg. apply (IHk (inter e f) (var x) b0 l n0) ; try omega ; assumption. Qed. Theorem sub_trans : forall a b c:formula, (sub a b) -> (sub b c) -> (sub a c). intros. assert (exists n : nat, sub_lg a b n). apply exists_length ; assumption. assert (exists m : nat, sub_lg b c m). apply exists_length ; assumption. inversion H1. inversion H2. apply (sub_trans_length (x + x0) a b c x x0) ; try omega ; assumption. Qed. (* Thanks to Hugo Herbelin *)