-
-
Save anonymous/4358785 to your computer and use it in GitHub Desktop.
cut-elimination theorem on LJp (propositional LJ, with single succedent).
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Require Import Coq.Lists.List. | |
| Require Import Coq.Sorting.Permutation. | |
| Require Import Coq.Relations.Relations. | |
| Require Import Coq.Classes.Morphisms. | |
| Require Import Coq.Setoids.Setoid. | |
| Require Import Coq.Arith.Arith. | |
| Require Import MyPermutations. | |
| Inductive PProp:Set := | |
| | PPbot : PProp | |
| | PPatom : nat -> PProp | |
| | PPimpl : PProp -> PProp -> PProp | |
| | PPconj : PProp -> PProp -> PProp | |
| | PPdisj : PProp -> PProp -> PProp. | |
| Lemma PProp_dec : forall p1 p2:PProp, {p1=p2} + {p1<>p2}. | |
| Proof. | |
| decide equality. | |
| apply eq_nat_dec. | |
| Qed. | |
| Instance In_compat_perm_PProp: | |
| Proper (eq ==> @Permutation PProp ==> iff) (@In PProp). | |
| Proof. | |
| apply In_compat_perm. | |
| apply PProp_dec. | |
| Qed. | |
| Inductive PProp_small(a b:PProp):Prop := | |
| | PPsmall_impl_l x: b = PPimpl a x -> PProp_small a b | |
| | PPsmall_impl_r x: b = PPimpl x a -> PProp_small a b | |
| | PPsmall_conj_l x: b = PPconj a x -> PProp_small a b | |
| | PPsmall_conj_r x: b = PPconj x a -> PProp_small a b | |
| | PPsmall_disj_l x: b = PPdisj a x -> PProp_small a b | |
| | PPsmall_disj_r x: b = PPdisj x a -> PProp_small a b. | |
| Arguments PPsmall_impl_l [a] [b] x H. | |
| Arguments PPsmall_impl_r [a] [b] x H. | |
| Arguments PPsmall_conj_l [a] [b] x H. | |
| Arguments PPsmall_conj_r [a] [b] x H. | |
| Arguments PPsmall_disj_l [a] [b] x H. | |
| Arguments PPsmall_disj_r [a] [b] x H. | |
| Lemma PProp_small_wellfounded: well_founded PProp_small. | |
| Proof. | |
| intros p. | |
| induction p. | |
| - exists. | |
| intros y Hy. | |
| destruct Hy as [z Hz|z Hz|z Hz|z Hz|z Hz|z Hz]; congruence. | |
| - exists. | |
| intros y Hy. | |
| destruct Hy as [z Hz|z Hz|z Hz|z Hz|z Hz|z Hz]; congruence. | |
| - exists. | |
| intros y Hy. | |
| destruct Hy as [z Hz|z Hz|z Hz|z Hz|z Hz|z Hz]; congruence. | |
| - exists. | |
| intros y Hy. | |
| destruct Hy as [z Hz|z Hz|z Hz|z Hz|z Hz|z Hz]; congruence. | |
| - exists. | |
| intros y Hy. | |
| destruct Hy as [z Hz|z Hz|z Hz|z Hz|z Hz|z Hz]; congruence. | |
| Qed. | |
| Inductive LJ_provable : list PProp -> PProp -> Prop := | |
| | LJ_perm P1 L1 L2 : | |
| Permutation L1 L2 -> | |
| LJ_provable L1 P1 -> | |
| LJ_provable L2 P1 | |
| | LJ_weak P1 P2 L1 : | |
| LJ_provable L1 P2 -> | |
| LJ_provable (P1::L1) P2 | |
| | LJ_contr P1 P2 L1 : | |
| LJ_provable (P1::P1::L1) P2 -> | |
| LJ_provable (P1::L1) P2 | |
| | LJ_axiom P1 : | |
| LJ_provable (P1::nil) P1 | |
| | LJ_exfalso P1 : | |
| LJ_provable (PPbot::nil) P1 | |
| | LJ_impl_antecedent P1 P2 P3 L1 : | |
| LJ_provable (L1) P1 -> | |
| LJ_provable (P2::L1) P3 -> | |
| LJ_provable (PPimpl P1 P2::L1) P3 | |
| | LJ_impl_succedent P1 P2 L1 : | |
| LJ_provable (P1::L1) P2 -> | |
| LJ_provable L1 (PPimpl P1 P2) | |
| | LJ_conj_antecedent P1 P2 P3 L1 : | |
| LJ_provable (P1::P2::L1) P3 -> | |
| LJ_provable (PPconj P1 P2::L1) P3 | |
| | LJ_conj_succedent P1 P2 L1 : | |
| LJ_provable L1 P1 -> | |
| LJ_provable L1 P2 -> | |
| LJ_provable L1 (PPconj P1 P2) | |
| | LJ_disj_antecedent P1 P2 P3 L1 : | |
| LJ_provable (P1::L1) P3 -> | |
| LJ_provable (P2::L1) P3 -> | |
| LJ_provable (PPdisj P1 P2::L1) P3 | |
| | LJ_disj_succedent_l P1 P2 L1 : | |
| LJ_provable L1 P1 -> | |
| LJ_provable L1 (PPdisj P1 P2) | |
| | LJ_disj_succedent_r P1 P2 L1 : | |
| LJ_provable L1 P2 -> | |
| LJ_provable L1 (PPdisj P1 P2). | |
| Ltac LJ_reorder_antecedent L := | |
| apply (LJ_perm _ L); [perm|]. | |
| Instance LJ_provable_compat : Proper (@Permutation _==>eq==>iff) LJ_provable. | |
| Proof. | |
| unfold Proper,respectful. | |
| intros L1 L2 HL P1 P2 HP. | |
| split. | |
| - intros H. | |
| rewrite <-HP. | |
| exact (LJ_perm P1 L1 L2 HL H). | |
| - intros H. | |
| rewrite ->HP. | |
| exact (LJ_perm P2 L2 L1 (Permutation_sym HL) H). | |
| Qed. | |
| Lemma LJ_weakN: forall P1 L1 L2, LJ_provable L1 P1 -> LJ_provable (L2++L1) P1. | |
| Proof. | |
| intros P1 L1 L2 H. | |
| induction L2. | |
| - exact H. | |
| - apply LJ_weak,IHL2. | |
| Qed. | |
| Lemma LJ_contrN: forall P1 L1 L2, LJ_provable (L2++L2++L1) P1 -> LJ_provable (L2++L1) P1. | |
| Proof. | |
| intros P1 L1 L2 H. | |
| revert L1 H. | |
| induction L2. | |
| - intros L1 H. | |
| exact H. | |
| - intros L1 H. | |
| LJ_reorder_antecedent (L2++(a::L1)). | |
| apply IHL2. | |
| LJ_reorder_antecedent (a::L2++L2++L1). | |
| apply LJ_contr. | |
| LJ_reorder_antecedent ((a::L2)++(a::L2)++L1). | |
| exact H. | |
| Qed. | |
| Lemma LJ_bot_elim: forall P1 L1, LJ_provable L1 PPbot -> LJ_provable L1 P1. | |
| Proof. | |
| intros P1 L1 H. | |
| remember PPbot as P2 in H. | |
| induction H. | |
| - rewrite <-H. | |
| apply IHLJ_provable,HeqP2. | |
| - apply LJ_weak,IHLJ_provable,HeqP2. | |
| - apply LJ_contr,IHLJ_provable,HeqP2. | |
| - rewrite HeqP2. | |
| apply LJ_exfalso. | |
| - apply LJ_exfalso. | |
| - apply LJ_impl_antecedent. | |
| + apply H. | |
| + apply IHLJ_provable2,HeqP2. | |
| - congruence. | |
| - apply LJ_conj_antecedent,IHLJ_provable,HeqP2. | |
| - congruence. | |
| - apply LJ_disj_antecedent. | |
| + apply IHLJ_provable1,HeqP2. | |
| + apply IHLJ_provable2,HeqP2. | |
| - congruence. | |
| - congruence. | |
| Qed. | |
| Lemma LJ_conj_elim_l: | |
| forall P1 P2 L1, | |
| LJ_provable L1 (PPconj P1 P2) -> LJ_provable L1 P1. | |
| Proof. | |
| intros P1 P2 L1 H. | |
| remember (PPconj P1 P2) as P3 in H. | |
| induction H. | |
| - rewrite <-H. | |
| apply IHLJ_provable,HeqP3. | |
| - apply LJ_weak,IHLJ_provable,HeqP3. | |
| - apply LJ_contr,IHLJ_provable,HeqP3. | |
| - rewrite HeqP3. | |
| apply LJ_conj_antecedent. | |
| LJ_reorder_antecedent (P2::P1::nil). | |
| apply LJ_weak. | |
| apply LJ_axiom. | |
| - apply LJ_exfalso. | |
| - apply LJ_impl_antecedent. | |
| + apply H. | |
| + apply IHLJ_provable2,HeqP3. | |
| - congruence. | |
| - apply LJ_conj_antecedent,IHLJ_provable,HeqP3. | |
| - congruence. | |
| - apply LJ_disj_antecedent. | |
| + apply IHLJ_provable1,HeqP3. | |
| + apply IHLJ_provable2,HeqP3. | |
| - congruence. | |
| - congruence. | |
| Qed. | |
| Lemma LJ_conj_elim_r: | |
| forall P1 P2 L1, | |
| LJ_provable L1 (PPconj P1 P2) -> LJ_provable L1 P2. | |
| Proof. | |
| intros P1 P2 L1 H. | |
| remember (PPconj P1 P2) as P3 in H. | |
| induction H. | |
| - rewrite <-H. | |
| apply IHLJ_provable,HeqP3. | |
| - apply LJ_weak,IHLJ_provable,HeqP3. | |
| - apply LJ_contr,IHLJ_provable,HeqP3. | |
| - rewrite HeqP3. | |
| apply LJ_conj_antecedent. | |
| apply LJ_weak. | |
| apply LJ_axiom. | |
| - apply LJ_exfalso. | |
| - apply LJ_impl_antecedent. | |
| + apply H. | |
| + apply IHLJ_provable2,HeqP3. | |
| - congruence. | |
| - apply LJ_conj_antecedent,IHLJ_provable,HeqP3. | |
| - congruence. | |
| - apply LJ_disj_antecedent. | |
| + apply IHLJ_provable1,HeqP3. | |
| + apply IHLJ_provable2,HeqP3. | |
| - congruence. | |
| - congruence. | |
| Qed. | |
| Lemma LJ_impl_elim: | |
| forall P1 P2 L1, | |
| LJ_provable L1 (PPimpl P1 P2) -> LJ_provable (P1::L1) P2. | |
| Proof. | |
| intros P1 P2 L1 H. | |
| remember (PPimpl P1 P2) as P3 in H. | |
| induction H. | |
| - rewrite <-H. | |
| apply IHLJ_provable,HeqP3. | |
| - LJ_reorder_antecedent (P0::P1::L1). | |
| apply LJ_weak,IHLJ_provable,HeqP3. | |
| - LJ_reorder_antecedent (P0::P1::L1). | |
| apply LJ_contr. | |
| LJ_reorder_antecedent (P1::P0::P0::L1). | |
| apply IHLJ_provable,HeqP3. | |
| - rewrite HeqP3. | |
| LJ_reorder_antecedent (PPimpl P1 P2::P1::nil). | |
| apply LJ_impl_antecedent. | |
| + apply LJ_axiom. | |
| + LJ_reorder_antecedent (P1::P2::nil). | |
| apply LJ_weak,LJ_axiom. | |
| - apply LJ_weak,LJ_exfalso. | |
| - LJ_reorder_antecedent (PPimpl P0 P3::P1::L1). | |
| apply LJ_impl_antecedent. | |
| + apply LJ_weak,H. | |
| + LJ_reorder_antecedent (P1::P3::L1). | |
| apply IHLJ_provable2,HeqP3. | |
| - congruence. | |
| - LJ_reorder_antecedent (PPconj P0 P3::P1::L1). | |
| apply LJ_conj_antecedent. | |
| LJ_reorder_antecedent (P1::P0::P3::L1). | |
| apply IHLJ_provable,HeqP3. | |
| - congruence. | |
| - LJ_reorder_antecedent (PPdisj P0 P3::P1::L1). | |
| apply LJ_disj_antecedent. | |
| + LJ_reorder_antecedent (P1::P0::L1). | |
| apply IHLJ_provable1,HeqP3. | |
| + LJ_reorder_antecedent (P1::P3::L1). | |
| apply IHLJ_provable2,HeqP3. | |
| - congruence. | |
| - congruence. | |
| Qed. | |
| Fixpoint replicate{A:Type} (n:nat) (a:A):list A := | |
| match n with | |
| | O => nil | |
| | S n' => a :: replicate n' a | |
| end. | |
| Lemma In_replicate_eq: forall{A:Type} (a b:A) (n:nat), In a (replicate n b) -> a = b. | |
| Proof. | |
| intros A a b n. | |
| induction n. | |
| - intros []. | |
| - intros [H|H]. | |
| + congruence. | |
| + apply IHn,H. | |
| Qed. | |
| Lemma eq_then_Permutation: forall{A:Type} (l1 l2:list A), l1 = l2 -> Permutation l1 l2. | |
| Proof. | |
| intros A l1 l2 H. | |
| rewrite H; reflexivity. | |
| Qed. | |
| Lemma LJ_cut_permselect: | |
| forall(P1 P2:PProp) (L1 L2:list PProp) (n:nat), | |
| Permutation (P1::L1) (replicate n P2++L2) -> | |
| ( | |
| P1 = P2 /\ match n with | |
| | O => False | |
| | S n' => Permutation L1 (replicate n' P2++L2) | |
| end | |
| ) \/ ( | |
| exists L2', | |
| Permutation L2 (P1::L2') /\ | |
| Permutation L1 (replicate n P2++L2') | |
| ). | |
| Proof. | |
| intros P1 P2 L1 L2 n HP. | |
| assert (HI:=in_eq P1 L1). | |
| rewrite HP in HI. | |
| rewrite in_app_iff in HI. | |
| destruct HI as [HI|HI]. | |
| - left. | |
| split. | |
| + apply In_replicate_eq in HI. | |
| exact HI. | |
| + destruct n as [|n]. | |
| * contradict HI. | |
| * apply In_replicate_eq in HI. | |
| rewrite HI in HP. | |
| apply Permutation_cons_inv with (a:=P2). | |
| exact HP. | |
| - right. | |
| destruct (in_split _ _ HI) as (L2A,(L2B,HL2)). | |
| exists (L2A++L2B). | |
| split. | |
| + rewrite HL2. | |
| perm. | |
| + apply Permutation_cons_inv with (a:=P1). | |
| rewrite HP. | |
| rewrite HL2. | |
| perm. | |
| Qed. | |
| Lemma LJ_cut_permselect_nil: | |
| forall(P1 P2:PProp) (L2:list PProp) (n:nat), | |
| Permutation (P1::nil) (replicate n P2++L2) -> | |
| ( | |
| P1 = P2 /\ n = 1 /\ L2 = nil | |
| ) \/ ( | |
| n = 0 /\ L2 = (P1::nil) | |
| ). | |
| intros P1 P2 L2 n HP. | |
| apply Permutation_length_1_inv in HP. | |
| destruct n as [|n]. | |
| - right. | |
| split. | |
| + reflexivity. | |
| + exact HP. | |
| - left. | |
| change (P2::(replicate n P2++L2) = P1::nil) in HP. | |
| split. | |
| { | |
| congruence. | |
| } | |
| assert (HP2: replicate n P2++L2 = nil) by congruence. | |
| destruct n as [|n]; simpl in HP2; [|congruence]. | |
| split. | |
| + reflexivity. | |
| + exact HP2. | |
| Qed. | |
| Lemma LJ_disj_elim2_withcut: | |
| forall P1 P2 P3 L1 L2, | |
| (forall PA LA1 LA2, | |
| LJ_provable LA1 P1 -> LJ_provable (P1::LA2) PA -> LJ_provable (LA1++LA2) PA) -> | |
| (forall PA LA1 LA2, | |
| LJ_provable LA1 P2 -> LJ_provable (P2::LA2) PA -> LJ_provable (LA1++LA2) PA) -> | |
| LJ_provable L1 (PPdisj P1 P2) -> | |
| LJ_provable (P1::L2) P3 -> | |
| LJ_provable (P2::L2) P3 -> | |
| LJ_provable (L1++L2) P3. | |
| Proof. | |
| intros P1 P2 P3 L1 L2 Hcut1 Hcut2 HC HP1 HP2. | |
| remember (PPdisj P1 P2) as P4 in HC. | |
| induction HC. | |
| - rewrite <-H. | |
| apply IHHC,HeqP4. | |
| - apply LJ_weak,IHHC,HeqP4. | |
| - apply LJ_contr,IHHC,HeqP4. | |
| - rewrite HeqP4; simpl. | |
| apply LJ_disj_antecedent. | |
| + exact HP1. | |
| + exact HP2. | |
| - setoid_replace ((PPbot::nil)++L2) with (L2++(PPbot::nil)); [|perm]. | |
| apply LJ_weakN. | |
| apply LJ_exfalso. | |
| - apply LJ_impl_antecedent. | |
| + change (LJ_provable (L1++L2) P0). | |
| setoid_replace (L1++L2) with (L2++L1); [|perm]. | |
| apply LJ_weakN. | |
| exact HC1. | |
| + change (LJ_provable (P4::L1++L2) P3). | |
| apply IHHC2,HeqP4. | |
| - congruence. | |
| - apply LJ_conj_antecedent. | |
| apply IHHC,HeqP4. | |
| - congruence. | |
| - apply LJ_disj_antecedent. | |
| + apply IHHC1,HeqP4. | |
| + apply IHHC2,HeqP4. | |
| - apply Hcut1. | |
| + replace P1 with P0 by congruence. | |
| exact HC. | |
| + exact HP1. | |
| - apply Hcut2. | |
| + replace P2 with P4 by congruence. | |
| exact HC. | |
| + exact HP2. | |
| Qed. | |
| Lemma LJ_cut_general: | |
| forall P1 P2 L1 L2 n, | |
| LJ_provable L1 P1 -> | |
| LJ_provable (replicate n P1++L2) P2 -> | |
| LJ_provable (L1++L2) P2. | |
| Proof. | |
| induction P1 as (KP1,HI_rank) using (well_founded_ind PProp_small_wellfounded). | |
| intros KP2 KL1 KL2 n HPrL HPrR. | |
| remember (replicate n KP1 ++ KL2) as KL3 in HPrR. | |
| assert (HKL3: Permutation KL3 (replicate n KP1 ++ KL2)) by (rewrite HeqKL3; reflexivity). | |
| clear HeqKL3. | |
| revert KL1 KL2 n HKL3 HPrL. | |
| induction HPrR. | |
| - intros KL1 KL2 n HKL3 HPrL. | |
| apply IHHPrR with (n:=n). | |
| + transitivity L2; tauto. | |
| + exact HPrL. | |
| - intros KL1 KL2 n HKL3 HPrL. | |
| apply LJ_cut_permselect in HKL3. | |
| destruct HKL3 as [(PrA,PrB) | (KL2',(PrC,PrD))]. | |
| + destruct n as [|n]; [contradict PrB|]. | |
| apply IHHPrR with (n:=n). | |
| * exact PrB. | |
| * exact HPrL. | |
| + rewrite PrC. | |
| LJ_reorder_antecedent (P1::KL1++KL2'). | |
| apply LJ_weak. | |
| apply IHHPrR with (n:=n). | |
| * exact PrD. | |
| * exact HPrL. | |
| - intros KL1 KL2 n HKL3 HPrL. | |
| apply LJ_cut_permselect in HKL3. | |
| destruct HKL3 as [(PrA,PrB) | (KL2',(PrC,PrD))]. | |
| + destruct n as [|n]; [contradict PrB|]. | |
| apply IHHPrR with (n:=S (S n)). | |
| * rewrite PrA. | |
| do 2 apply Permutation_cons. | |
| exact PrB. | |
| * exact HPrL. | |
| + rewrite PrC. | |
| LJ_reorder_antecedent (P1::KL1++KL2'). | |
| apply LJ_contr. | |
| LJ_reorder_antecedent (KL1++(P1::P1::KL2')). | |
| apply IHHPrR with (n:=n). | |
| * rewrite PrD. | |
| perm. | |
| * exact HPrL. | |
| - intros KL1 KL2 n HKL3 HPrL. | |
| apply LJ_cut_permselect_nil in HKL3. | |
| destruct HKL3 as [(PrA,(PrB,PrC)) | (PrD,PrE)]. | |
| + rewrite PrA,PrC,app_nil_r. | |
| exact HPrL. | |
| + rewrite PrE. | |
| apply LJ_weakN. | |
| apply LJ_axiom. | |
| - intros KL1 KL2 n HKL3 HPrL. | |
| apply LJ_cut_permselect_nil in HKL3. | |
| destruct HKL3 as [(PrA,(PrB,PrC)) | (PrD,PrE)]. | |
| + rewrite PrC,app_nil_r. | |
| apply LJ_bot_elim. | |
| rewrite PrA. | |
| exact HPrL. | |
| + rewrite PrE. | |
| apply LJ_weakN. | |
| apply LJ_exfalso. | |
| - intros KL1 KL2 n HKL3 HPrL. | |
| apply LJ_cut_permselect in HKL3. | |
| destruct HKL3 as [(PrA,PrB) | (KL2',(PrC,PrD))]. | |
| + destruct n as [|n]; [contradict PrB|]. | |
| { | |
| LJ_reorder_antecedent (KL1++KL2). | |
| do 2 apply LJ_contrN. | |
| LJ_reorder_antecedent (KL2++KL1++KL1++KL1). | |
| apply LJ_contrN. | |
| LJ_reorder_antecedent (((KL1++KL2)++KL1)++(KL1++KL2)). | |
| apply HI_rank with (y:=P2) (n:=1). | |
| - apply (PPsmall_impl_r _ (eq_sym PrA)). | |
| - apply HI_rank with (y:=P1) (n:=1). | |
| + apply (PPsmall_impl_l _ (eq_sym PrA)). | |
| + apply IHHPrR1 with (n:=n). | |
| * exact PrB. | |
| * exact HPrL. | |
| + apply LJ_impl_elim. | |
| rewrite PrA. | |
| exact HPrL. | |
| - simpl. | |
| LJ_reorder_antecedent (KL1 ++ (P2::KL2)). | |
| apply IHHPrR2 with (n:=n). | |
| + rewrite PrB; perm. | |
| + exact HPrL. | |
| } | |
| + rewrite PrC. | |
| LJ_reorder_antecedent (PPimpl P1 P2 :: KL1 ++ KL2'). | |
| { | |
| apply LJ_impl_antecedent. | |
| - apply IHHPrR1 with (n:=n). | |
| + exact PrD. | |
| + exact HPrL. | |
| - LJ_reorder_antecedent (KL1 ++ P2 :: KL2'). | |
| apply IHHPrR2 with (n:=n). | |
| + rewrite PrD; perm. | |
| + exact HPrL. | |
| } | |
| - intros KL1 KL2 n HKL3 HPrL. | |
| apply LJ_impl_succedent. | |
| LJ_reorder_antecedent (KL1 ++ P1 :: KL2). | |
| apply IHHPrR with (n:=n). | |
| + rewrite HKL3; perm. | |
| + exact HPrL. | |
| - intros KL1 KL2 n HKL3 HPrL. | |
| apply LJ_cut_permselect in HKL3. | |
| destruct HKL3 as [(PrA,PrB) | (KL2',(PrC,PrD))]. | |
| + destruct n as [|n]; [contradict PrB|]. | |
| { | |
| do 2 apply LJ_contrN. | |
| apply HI_rank with (y:=P2) (n:=1). | |
| - apply (PPsmall_conj_r _ (eq_sym PrA)). | |
| - apply LJ_conj_elim_r with (P1:=P1). | |
| rewrite PrA. | |
| exact HPrL. | |
| - simpl; LJ_reorder_antecedent (KL1 ++ P2 :: KL1 ++ KL2). | |
| apply HI_rank with (y:=P1) (n:=1). | |
| + apply (PPsmall_conj_l _ (eq_sym PrA)). | |
| + apply LJ_conj_elim_l with (P2:=P2). | |
| rewrite PrA. | |
| exact HPrL. | |
| + simpl; LJ_reorder_antecedent (KL1 ++ P1 :: P2 :: KL2). | |
| apply IHHPrR with (n:=n). | |
| * rewrite PrB; perm. | |
| * exact HPrL. | |
| } | |
| + rewrite PrC. | |
| LJ_reorder_antecedent (PPconj P1 P2 :: KL1 ++ KL2'). | |
| apply LJ_conj_antecedent. | |
| LJ_reorder_antecedent (KL1 ++ P1 :: P2 :: KL2'). | |
| apply IHHPrR with (n:=n). | |
| * rewrite PrD; perm. | |
| * exact HPrL. | |
| - intros KL1 KL2 n HKL3 HPrL. | |
| apply LJ_conj_succedent. | |
| + apply IHHPrR1 with (n:=n). | |
| * exact HKL3. | |
| * exact HPrL. | |
| + apply IHHPrR2 with (n:=n). | |
| * exact HKL3. | |
| * exact HPrL. | |
| - intros KL1 KL2 n HKL3 HPrL. | |
| apply LJ_cut_permselect in HKL3. | |
| destruct HKL3 as [(PrA,PrB) | (KL2',(PrC,PrD))]. | |
| + destruct n as [|n]; [contradict PrB|]. | |
| { | |
| apply LJ_contrN. | |
| apply LJ_disj_elim2_withcut with (P1:=P1) (P2:=P2). | |
| - intros PA LA1 LA2 HA1 HA2. | |
| apply HI_rank with (y:=P1) (n:=1). | |
| + apply (PPsmall_disj_l _ (eq_sym PrA)). | |
| + exact HA1. | |
| + exact HA2. | |
| - intros PA LA1 LA2 HA1 HA2. | |
| apply HI_rank with (y:=P2) (n:=1). | |
| + apply (PPsmall_disj_r _ (eq_sym PrA)). | |
| + exact HA1. | |
| + exact HA2. | |
| - rewrite PrA. | |
| exact HPrL. | |
| - LJ_reorder_antecedent (KL1 ++ P1 :: KL2). | |
| apply IHHPrR1 with (n:=n). | |
| + rewrite PrB; perm. | |
| + exact HPrL. | |
| - LJ_reorder_antecedent (KL1 ++ P2 :: KL2). | |
| apply IHHPrR2 with (n:=n). | |
| + rewrite PrB; perm. | |
| + exact HPrL. | |
| } | |
| + rewrite PrC. | |
| { | |
| LJ_reorder_antecedent (PPdisj P1 P2 :: KL1 ++ KL2'). | |
| apply LJ_disj_antecedent. | |
| - LJ_reorder_antecedent (KL1 ++ P1 :: KL2'). | |
| apply IHHPrR1 with (n:=n). | |
| + rewrite PrD; perm. | |
| + exact HPrL. | |
| - LJ_reorder_antecedent (KL1 ++ P2 :: KL2'). | |
| apply IHHPrR2 with (n:=n). | |
| + rewrite PrD; perm. | |
| + exact HPrL. | |
| } | |
| - intros KL1 KL2 n HKL3 HPrL. | |
| apply LJ_disj_succedent_l. | |
| apply IHHPrR with (n:=n). | |
| + exact HKL3. | |
| + exact HPrL. | |
| - intros KL1 KL2 n HKL3 HPrL. | |
| apply LJ_disj_succedent_r. | |
| apply IHHPrR with (n:=n). | |
| + exact HKL3. | |
| + exact HPrL. | |
| Qed. | |
| Lemma LJ_cut2: | |
| forall P1 P2 L1 L2, | |
| LJ_provable L1 P1 -> | |
| LJ_provable (P1::L2) P2 -> | |
| LJ_provable (L1++L2) P2. | |
| Proof. | |
| intros P1 P2 L1 L2. | |
| apply LJ_cut_general with (n:=1). | |
| Qed. | |
| Theorem LJ_cut: | |
| forall P1 P2 L1, | |
| LJ_provable L1 P1 -> | |
| LJ_provable (P1::L1) P2 -> | |
| LJ_provable L1 P2. | |
| Proof. | |
| intros P1 P2 L1 HPrL HPrR. | |
| rewrite (app_nil_end L1). | |
| apply LJ_contrN. | |
| rewrite app_nil_r. | |
| revert HPrL HPrR. | |
| apply LJ_cut2. | |
| Qed. | |
| Lemma LJ_disj_elim2: | |
| forall P1 P2 P3 L1 L2, | |
| LJ_provable L1 (PPdisj P1 P2) -> | |
| LJ_provable (P1::L2) P3 -> | |
| LJ_provable (P2::L2) P3 -> | |
| LJ_provable (L1++L2) P3. | |
| Proof. | |
| intros P1 P2 P3 L1 L2. | |
| apply LJ_disj_elim2_withcut. | |
| - intros PA LA1 LA2. | |
| apply LJ_cut2. | |
| - intros PA LA1 LA2. | |
| apply LJ_cut2. | |
| Qed. | |
| Lemma LJ_disj_elim: | |
| forall P1 P2 P3 L1, | |
| LJ_provable L1 (PPdisj P1 P2) -> | |
| LJ_provable (P1::L1) P3 -> | |
| LJ_provable (P2::L1) P3 -> | |
| LJ_provable L1 P3. | |
| Proof. | |
| intros P1 P2 P3 L1 HPrL HPrR1 HPrR2. | |
| rewrite (app_nil_end L1). | |
| apply LJ_contrN. | |
| rewrite app_nil_r. | |
| revert HPrL HPrR1 HPrR2. | |
| apply LJ_disj_elim2. | |
| Qed. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Require Import Coq.Lists.List. | |
| Require Import Coq.Sorting.Permutation. | |
| Require Import Coq.Relations.Relations. | |
| Require Import Coq.Classes.Morphisms. | |
| Require Import Coq.Setoids.Setoid. | |
| Lemma app_compat_perm_latter(A:Type) : forall l a1 a2:list A, Permutation a1 a2 -> Permutation (l++a1) (l++a2). | |
| Proof. | |
| intros l a1 a2 Ha. | |
| induction l. | |
| - exact Ha. | |
| - apply perm_skip,IHl. | |
| Qed. | |
| Instance app_compat_perm(A:Type) : Proper (@Permutation A ==> @Permutation A ==> @Permutation A) (@app A). | |
| Proof. | |
| unfold Proper,respectful. | |
| intros a1 a2 Ha b1 b2 Hb. | |
| induction Ha. | |
| - exact Hb. | |
| - apply perm_skip. | |
| exact IHHa. | |
| - apply perm_trans with ((x::y::l)++b1). | |
| + apply perm_swap. | |
| + apply perm_skip,perm_skip,app_compat_perm_latter,Hb. | |
| - apply perm_trans with (l'++b2); [exact IHHa1|]. | |
| apply perm_trans with (l'++b1); [|exact IHHa2]. | |
| apply app_compat_perm_latter,Permutation_sym,Hb. | |
| Qed. | |
| Lemma Permutation_In_In: forall{A:Type} (x:A) (l1 l2:list A), Permutation l1 l2 -> In x l1 -> In x l2. | |
| Proof. | |
| intros A x l1 l2 HP H. | |
| induction HP. | |
| - exact H. | |
| - destruct H as [H|H]. | |
| + left. | |
| exact H. | |
| + right. | |
| apply IHHP,H. | |
| - destruct H as [H|[H|H]]. | |
| + right. | |
| left. | |
| exact H. | |
| + left. | |
| exact H. | |
| + right. | |
| right. | |
| exact H. | |
| - apply IHHP2,IHHP1,H. | |
| Qed. | |
| Instance In_compat_perm(A:Type) | |
| (eq_dec: forall x y:A, {x=y} + {x<>y}): | |
| Proper (eq ==> @Permutation A ==> iff) (@In A). | |
| Proof. | |
| unfold Proper,respectful. | |
| intros x1 x2 Hx l1 l2 Hl. | |
| rewrite Hx; clear x1 Hx. | |
| split. | |
| - apply Permutation_In_In,Hl. | |
| - apply Permutation_In_In. | |
| symmetry. | |
| exact Hl. | |
| Qed. | |
| Lemma app_normalize_1: | |
| forall(A:Type) (l1 l2 l3:list A), | |
| (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3). | |
| Proof. | |
| intros A l1 l2 l3. | |
| rewrite app_assoc. | |
| reflexivity. | |
| Qed. | |
| Lemma app_normalize_2: | |
| forall(A:Type) (a1:A) (l2 l3:list A), | |
| (a1 :: l2) ++ l3 = a1 :: (l2 ++ l3). | |
| Proof. | |
| intros; reflexivity. | |
| Qed. | |
| Lemma app_normalize_3: | |
| forall(A:Type) (l1:list A), (nil++l1) = l1. | |
| Proof. | |
| intros; reflexivity. | |
| Qed. | |
| Ltac app_normalize := repeat ( | |
| rewrite app_normalize_1 || | |
| rewrite app_normalize_2 || | |
| rewrite app_normalize_3). | |
| Lemma perm_takeit_1: | |
| forall(A:Type) (target:list A) (l1 l2:list A), | |
| Permutation (l1 ++ (target ++ l2)) (target ++ (l1 ++ l2)). | |
| Proof. | |
| intros A target l1 l2. | |
| rewrite (app_assoc l1 target l2), | |
| (Permutation_app_comm l1 target), | |
| <-(app_assoc target l1 l2). | |
| reflexivity. | |
| Qed. | |
| Lemma perm_takeit_2: | |
| forall(A:Type) (target:list A) (a1:A) (l2:list A), | |
| Permutation (a1 :: (target ++ l2)) (target ++ (a1 :: l2)). | |
| Proof. | |
| intros A target a1 l2. | |
| apply (perm_takeit_1 _ _ (a1::nil)). | |
| Qed. | |
| Lemma perm_takeit_3: | |
| forall(A:Type) (target:list A) (l1:list A), | |
| Permutation (l1 ++ target) (target ++ l1). | |
| Proof. | |
| intros A target l1. | |
| apply Permutation_app_comm. | |
| Qed. | |
| Lemma perm_takeit_4: | |
| forall(A:Type) (target:list A) (a1:A), | |
| Permutation (a1 :: target) (target ++ (a1::nil)). | |
| Proof. | |
| intros A target a1. | |
| apply (perm_takeit_3 _ _ (a1::nil)). | |
| Qed. | |
| Lemma perm_takeit_5: | |
| forall(A:Type) (target:A) (l1 l2:list A), | |
| Permutation (l1 ++ (target :: l2)) (target :: (l1 ++ l2)). | |
| Proof. | |
| intros A target l1 l2. | |
| apply (perm_takeit_1 _ (target::nil)). | |
| Qed. | |
| Lemma perm_takeit_6: | |
| forall(A:Type) (target:A) (a1:A) (l2:list A), | |
| Permutation (a1 :: (target :: l2)) (target :: (a1 :: l2)). | |
| Proof. | |
| intros A target a1 l2. | |
| apply (perm_takeit_2 _ (target::nil)). | |
| Qed. | |
| Lemma perm_takeit_7: | |
| forall(A:Type) (target:A) (l1:list A), | |
| Permutation (l1 ++ (target::nil)) (target :: l1). | |
| Proof. | |
| intros A target l1. | |
| apply (perm_takeit_3 _ (target::nil)). | |
| Qed. | |
| Lemma perm_takeit_8: | |
| forall(A:Type) (target:A) (a1:A), | |
| Permutation (a1 :: (target::nil)) (target :: (a1::nil)). | |
| Proof. | |
| intros A target a1. | |
| apply (perm_takeit_4 _ (target::nil)). | |
| Qed. | |
| Ltac perm_simplify := app_normalize; repeat ( | |
| rewrite app_nil_r || | |
| match goal with | |
| | [ |- Permutation ?L1 ?L1 ] => reflexivity | |
| | [ |- Permutation (?A1++_) (?A1++_) ] => apply Permutation_app_head | |
| | [ |- Permutation (?A1::_) (?A1::_) ] => apply perm_skip | |
| | [ |- Permutation _ (?L1++_) ] => ( | |
| rewrite (perm_takeit_1 _ L1) at 1 || | |
| rewrite (perm_takeit_2 _ L1) at 1 || | |
| rewrite (perm_takeit_3 _ L1) at 1 || | |
| rewrite (perm_takeit_4 _ L1) at 1 ) | |
| | [ |- Permutation _ (?A1::_) ] => ( | |
| rewrite (perm_takeit_5 _ A1) at 1 || | |
| rewrite (perm_takeit_6 _ A1) at 1 || | |
| rewrite (perm_takeit_7 _ A1) at 1 || | |
| rewrite (perm_takeit_8 _ A1) at 1 ) | |
| | [ |- Permutation _ _ ] => fail | |
| end). | |
| Ltac perm := | |
| match goal with | |
| | [ |- Permutation _ _ ] => perm_simplify; fail "perm failed" | |
| | [ |- _ ] => fail "perm can't solve this system." | |
| end. | |
| Lemma perm_test: forall(A:Type) | |
| (a b c d e f:A) | |
| (p q r s:list A), | |
| Permutation (a::q++c::(e::p++s)++r++d::r++f::b::q) ((p++c::q++r)++f::b::q++r++a::s++e::d::nil). | |
| Proof. | |
| intros. | |
| perm. | |
| Qed. | |
| Lemma perm_test2: forall(A:Type) | |
| (a b:list A), | |
| Permutation (a++b++b) (b++b++a). | |
| Proof. | |
| intros. | |
| perm. | |
| Qed. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment