(* Developed under The Coq Proof Assistant version 8.4pl4 *) (* with some unicode notations *) (* https://coq.inria.fr/ *) Require Import Relations. Require Import Morphisms. Require Import Omega. Require Import Psatz. (** Preliminaries **) (* Exponential *) (* function 2 ^ n *) Fixpoint exp n : nat := match n with | O => 1 | S n => exp n + exp n end. Lemma exp_pos : forall n, 0 < exp n . Proof. induction n ; simpl ; omega. Qed. Lemma exp_mon : forall n m, n <= m -> exp n <= exp m . Proof. intros n m H. induction H ; simpl ; lia. Qed. Lemma mon_max : forall f n m, (forall x y, x <= y -> f x <= f y) -> max (f n) (f m) <= f (max n m) . Proof with try (simpl ; nia). intros f m n Hmon. assert (Hd := le_lt_dec n m). destruct Hd. - assert (Hf := Hmon _ _ l). assert (max m n = m) as Hmax... rewrite Hmax... - assert (m <= n) as Ho... assert (Hf := Hmon _ _ Ho). assert (max m n = n) as Hmax... rewrite Hmax... Qed. (* If Computations *) (* case reasoning for functions depending on leb *) Ltac case_bool x y := remember (leb x y) as bb eqn:HHeq ; destruct bb ; apply eq_sym in HHeq ; [ apply leb_complete in HHeq | apply leb_complete_conv in HHeq ] . (* Finite Functions *) (* locally increasing functions are increasing *) Lemma inc_fun : forall f l, (forall n, S n < l -> f n < f (S n)) -> forall m n, m < l -> n < m -> f n < f m . Proof with try eassumption ; try omega. intros f l Hi m. induction m ; intros n Hl Hn... inversion Hn. - apply Hi... - assert (n < m) as Ho by omega. apply IHm in Ho... eapply lt_trans... apply Hi... Qed. (* increasing functions are injective *) Lemma injective_inc_fun : forall f l, (forall m n, m < l -> n < m -> f n < f m) -> forall n m, n < l -> m < l -> f n = f m -> n = m . Proof with try omega. intros f l Hi n m Hn Hm Hf. destruct (lt_eq_lt_dec n m) as [[Hs | He] | Hs]... - apply (Hi m n Hm) in Hs... - apply (Hi n m Hn) in Hs... Qed. (* injection from l to k implies l <= k *) Lemma bound_inj_fun : forall l k, (exists e, ((forall n, n < l -> e n < k) /\ (forall n m, n < l -> m < l -> e n = e m -> n = m))) -> l <= k . Proof with try omega. induction l. - intros... - intros k [e [Hb Hi]]. assert (0 < k /\ l <= pred k)... split. { assert (e l < k)... apply Hb... } apply IHl. exists (fun x => if leb (e x) (e l) then e x else pred (e x)). split. + intros n Hl. case_bool (e n) (e l). * assert (e l < k). apply Hb... assert (e n = e l -> False)... intro He. apply Hi in He... * assert (e n < k)... apply Hb... + intros n m Hn Hm. case_bool (e n) (e l) ; rename HHeq into HHeq' ; case_bool (e m) (e l)... * apply Hi... * intro H. assert (e n = e l -> False)... intro He. apply Hi in He... * intro H. assert (e m = e l -> False)... intro He. apply Hi in He... * intro He. apply Hi... Qed. (* Euclidean Division *) (* 0 remainder in Euclidean division *) Lemma uniq_euclid_0 : forall c s a b, b < s -> a * s + b = c * s -> b = 0 . Proof with try nia. induction c ; intros... destruct a... apply (IHc s a b)... Qed. Lemma uniq_euclid_divid : forall d c s a b, b < s -> d < s -> a * s + b = c * s + d -> b = d . Proof with try eassumption ; try nia. induction d ; intros c s a b Hb Hs He. - apply (uniq_euclid_0 c s a b)... - destruct b. + assert (S d = 0)... apply (uniq_euclid_0 a s c)... + assert (b = d)... apply (IHd c s a b)... Qed. (* Product Order on nat *) Definition lt_nat_nat v1 v2 : Prop := (fst v1 < fst v2) \/ ((fst v1 = fst v2) /\ (snd v1 < snd v2)) . (* Well_founded Product Order on nat *) Lemma wf_nat_nat : well_founded lt_nat_nat. Proof with assumption. intros [n1 n2]. revert n2. induction n1 using (well_founded_induction lt_wf) ; induction n2 using (well_founded_induction lt_wf). constructor. intros [n1' n2'] [Ho | Ho] ; simpl in Ho. - apply H... - destruct Ho as [L R] ; subst. apply H0... Qed. (* Axiom of Finite Choice *) Lemma fchoice_finite : forall l, forall R : nat -> nat -> Prop, (forall x, x < l -> exists y, R x y) -> (exists f, forall x, x < l -> R x (f x)). Proof with try omega. induction l ; intros R He. - exists (fun _ => 0). intros... - destruct (IHl R) as [g Hg]. + intros x Hl. apply He... + assert (l < S l) as Hl... apply He in Hl. destruct Hl as [y Hy]. exists (fun x => if leb (S x) l then g x else y). intros x Hl. case_bool (S x) l. * apply Hg... * assert (x = l)... subst. assumption. Qed. (* Pre-Orders and Lattices Hierarchy *) Class PreLattice {T} (leq : relation T) := { isorder :> PreOrder leq; sup : T -> T -> T; inf : T -> T -> T; te : T; be : T; sup_geq1 : forall x y, leq x (sup x y); sup_geq2 : forall x y, leq y (sup x y); sup_leq : forall x y z, leq x z -> leq y z -> leq (sup x y) z; inf_leq1 : forall x y, leq (inf x y) x; inf_leq2 : forall x y, leq (inf x y) y; inf_geq : forall x y z, leq z x -> leq z y -> leq z (inf x y); te_geq : forall x, leq x te; be_leq : forall x, leq be x }. Class PreInvolLattice {T} (leq : relation T) := { islattice :> PreLattice leq; perp : T -> T; invol_leq : forall x, leq (perp (perp x)) x; invol_geq : forall x, leq x (perp (perp x)); contrap : forall x y, leq (perp y) (perp x) <-> leq x y }. (* Definition 1.1 *) Class PreOrthoLattice {T} (leq : relation T) := { isinvollattice :> PreInvolLattice leq; compl : forall x, leq te (sup x (perp x)) }. (* Example 1.2 *) Inductive Hex : Set := | tt : Hex | xx : Hex | nx : Hex | yy : Hex | ny : Hex | bb : Hex . Definition hleq i j := match i,j with | bb,_ => True | _,tt => True | xx,xx => True | yy,yy => True | nx,nx => True | ny,ny => True | ny,xx => True | nx,yy => True | _,_ => False end. Example hexagon_ord : PreOrder hleq. Proof. split. - intro i ; destruct i ; unfold hleq ; apply I. - intros i j k h1 h2. destruct i ; destruct j ; destruct k ; unfold hleq in h1 ; unfold hleq in h2 ; unfold hleq ; try (now apply I) ; try (now inversion h1) ; try (now inversion h2). Defined. Definition hsup i j := match i,j with | bb,k => k | k,bb => k | xx,xx => xx | yy,yy => yy | nx,nx => nx | ny,ny => ny | ny,xx => xx | xx,ny => xx | nx,yy => yy | yy,nx => yy | _,_ => tt end. Definition hinf i j := match i,j with | tt,k => k | k,tt => k | xx,xx => xx | yy,yy => yy | nx,nx => nx | ny,ny => ny | ny,xx => ny | xx,ny => ny | nx,yy => nx | yy,nx => nx | _,_ => bb end. Example hexagon_lat : PreLattice hleq. Proof. split with hsup hinf tt bb. - apply hexagon_ord. - intros i j. destruct i ; destruct j ; unfold hsup ; simpl ; unfold hleq ; apply I. - intros i j. destruct i ; destruct j ; unfold hsup ; simpl ; unfold hleq ; apply I. - intros i j k h1 h2. destruct i ; destruct j ; destruct k ; unfold hsup ; simpl ; unfold hleq ; simpl ; simpl in h1 ; unfold hleq in h1 ; simpl in h1 ; simpl in h2 ; unfold hleq in h2 ; simpl in h2 ; try (now apply I) ; try (now inversion h1) ; try (now inversion h2). - intros i j. destruct i ; destruct j ; unfold hsup ; simpl ; unfold hleq ; apply I. - intros i j. destruct i ; destruct j ; unfold hsup ; simpl ; unfold hleq ; apply I. - intros i j k h1 h2. destruct i ; destruct j ; destruct k ; unfold hsup ; simpl ; unfold hleq ; simpl ; simpl in h1 ; unfold hleq in h1 ; simpl in h1 ; simpl in h2 ; unfold hleq in h2 ; simpl in h2 ; try (now apply I) ; try (now inversion h1) ; try (now inversion h2). - intro i. destruct i ; simpl ; unfold hleq ; apply I. - intro i. destruct i ; simpl ; unfold hleq ; apply I. Defined. Definition hperp i := match i with | bb => tt | tt => bb | xx => nx | nx => xx | yy => ny | ny => yy end. Example hexagon_il : PreInvolLattice hleq. Proof. split with hperp. - apply hexagon_lat. - intro i. destruct i ; simpl ; unfold hleq ; unfold hperp ; apply I. - intro i. destruct i ; simpl ; unfold hleq ; unfold hperp ; apply I. - intros i j. split ; intro h. + destruct i ; destruct j ; simpl in h ; unfold hleq in h ; simpl ; unfold hleq ; unfold hperp ; simpl ; try (now apply I) ; try (now inversion h). + destruct i ; destruct j ; simpl in h ; unfold hleq in h ; simpl ; unfold hleq ; unfold hperp ; simpl ; try (now apply I) ; try (now inversion h). Defined. Example hexagon_ol : PreOrthoLattice hleq. Proof. split with hexagon_il. intro i. destruct i ; simpl ; unfold hleq ; unfold hperp ; apply I. Defined. (* Example 1.3 *) Example example_1_3 {T leq} {OL : PreOrthoLattice (T:=T) leq} : forall x y, leq te (sup (sup (inf x y) (perp x)) (perp y)) . Proof. intros x y. eapply PreOrder_Transitive. - eapply PreOrder_Transitive. + apply compl. + apply sup_leq. * apply sup_geq1. * { (* 1 *) eapply PreOrder_Transitive. - eapply PreOrder_Transitive. + { apply contrap. apply inf_geq. - eapply PreOrder_Transitive. + apply contrap. apply sup_geq1. + apply invol_leq. - eapply PreOrder_Transitive. + apply contrap. apply sup_geq2. + apply invol_leq. } + apply invol_leq. - apply sup_geq2. } - { (* 3 *) apply sup_leq. - eapply PreOrder_Transitive. + apply sup_geq1. + apply sup_geq1. - (* 2 *) apply sup_leq. + eapply PreOrder_Transitive. * apply sup_geq2. * apply sup_geq1. + apply sup_geq2. } Qed. (** Formulas **) Parameter Atom : Set. Inductive formula : Set := | var : Atom -> formula | covar : Atom -> formula | top : formula | bot : formula | wedge : formula -> formula -> formula | vee : formula -> formula -> formula . Notation "'ν' A" := (var A) (at level 12). Notation "'κ' A" := (covar A) (at level 12). Notation "⊤" := (top) (at level 10). Notation "⊥" := (bot) (at level 10). Notation "A ∧ B" := (wedge A B) (at level 16, left associativity). Notation "A ∨ B" := (vee A B) (at level 17, left associativity). Fixpoint dual A := match A with | var x => covar x | covar x => var x | top => bot | bot => top | wedge A B => vee (dual A) (dual B) | vee A B => wedge (dual A) (dual B) end. Notation "¬ A" := (dual A) (at level 10). Lemma bidual : forall A, dual (dual A) = A . Proof. induction A ; simpl ; try rewrite IHA1 ; try rewrite IHA2 ; reflexivity. Qed. Lemma codual : forall A B, dual A = B <-> A = dual B . Proof. intros A B ; split ; intro H. - rewrite <- bidual at 1. rewrite H. reflexivity. - rewrite <- bidual. rewrite H. reflexivity. Qed. Fixpoint fsize A := match A with | var x => 1 | covar x => 1 | top => 1 | bot => 1 | wedge A B => S (fsize A + fsize B) | vee A B => S (fsize A + fsize B) end. Notation "⎹ A ⎸" := (fsize A). Lemma fsize_pos : forall A, 0 < fsize A . Proof. induction A ; simpl ; omega. Qed. Lemma fsize_dual : forall A, fsize (dual A) = fsize A . Proof. induction A ; simpl ; try rewrite IHA1 ; try rewrite IHA2 ; reflexivity. Qed. Inductive is_var : formula -> Prop := | is_var_var : forall x, is_var (var x) . Inductive is_covar : formula -> Prop := | is_covar_covar : forall x, is_covar (covar x) . Lemma is_var_dual : forall A, is_var (dual A) <-> is_covar A . Proof. intro A. split ; intro H ; inversion H as [x H']. - apply codual in H'. subst ; simpl ; constructor. - constructor. Qed. Lemma is_covar_dual : forall A, is_covar (dual A) <-> is_var A . Proof. intro A. split ; intro H ; inversion H as [x H']. - apply codual in H'. subst ; simpl ; constructor. - constructor. Qed. Inductive is_vee : formula -> Prop := | is_vee_vee : forall A B, is_vee (vee A B) . Lemma is_vee_is_vee : forall A, is_vee A <-> exists B C, A = vee B C . Proof. intro A. split ; intro H. - inversion H. eexists ; eexists. reflexivity. - destruct H as [B [C Heq]]. subst. constructor. Qed. Inductive sync : formula -> Prop := | var_sync : forall x, sync (var x) | bot_sync : sync bot | vee_sync : forall A B, sync (vee A B) . Inductive async : formula -> Prop := | covar_async : forall x, async (covar x) | top_async : async top | wedge_async : forall A B, async (wedge A B) . Lemma sync_or_async : forall A, {sync A} + {async A} . Proof. induction A ; try (now left ; constructor) ; try (now right ; constructor). Qed. Lemma async_dual : forall A, async (dual A) <-> sync A . Proof. intro A ; split ; induction A ; intro Hs ; simpl ; try now inversion Hs ; constructor. Qed. Lemma sync_dual : forall A, sync (dual A) <-> async A . Proof. intro A ; split ; induction A ; intro Hs ; simpl ; try now inversion Hs ; constructor. Qed. (* automatic solving of properties about sync and async *) Ltac auto_sync_async := match goal with | |- sync (var _) => apply var_sync | |- sync bot => apply bot_sync | |- sync (vee _ _) => apply vee_sync | |- async (covar _) => apply covar_async | |- async top => apply top_async | |- async (wedge _ _) => apply wedge_async | |- sync (dual _) => progress simpl ; auto_sync_async | |- async (dual _) => progress simpl ; auto_sync_async | |- sync (dual _) => apply sync_dual ; auto_sync_async | |- async (dual _) => apply async_dual ; auto_sync_async | |- is_var (var _) => apply is_var_var | |- is_covar (covar _) => apply is_covar_covar | |- is_var (dual _) => apply is_var_dual ; auto_sync_async | |- is_covar (dual _) => apply is_covar_dual ; auto_sync_async | |- _ \/ _ => try (left ; auto_sync_async) ; try (right ; auto_sync_async) | |- _ /\ _ => try (split ; auto_sync_async) | _ => now assumption end. (** System OL **) (* Definition of OL *) (* pax, pctr and pwk are parameters for variants of the system *) (* pax specifies formulas for which axiom is allowed *) (* pctr specifies formulas for which contraction is allowed *) (* pwk specifies formulas for which weakening is allowed *) Inductive ol {pax pctr pwk : formula -> Prop} : formula -> formula -> Prop := | ax_ol : forall A, pax A -> ol (dual A) A | top_ol : forall C, ol top C | wedge_ol : forall A B C, ol A C -> ol B C -> ol (wedge A B) C | vee_l_ol : forall A B C, ol A C -> ol (vee A B) C | vee_r_ol : forall A B C, ol A C -> ol (vee B A) C | cw_ol : forall A B, pctr A -> pwk B -> ol A A -> ol A B | ex_ol : forall A B, ol A B -> ol B A . Lemma not_var_var_ol : forall x y pax pctr pwk, ~ @ol pax pctr pwk (var x) (var y) . Proof. intros x y pax pctr pwk pi. remember (var x) as A. remember (var y) as B. revert x y HeqA HeqB ; induction pi ; intros x y HeqA HeqB ; subst ; try (now inversion HeqA) ; try (now eapply IHpi ; reflexivity). Qed. Lemma not_covar_covar_ol : forall x y pax pctr pwk, ~ @ol pax pctr pwk (covar x) (covar y) . Proof. intros x y pax pctr pwk pi. remember (covar x) as A. remember (covar y) as B. revert x y HeqA HeqB ; induction pi ; intros x y HeqA HeqB ; subst ; try (now inversion HeqA) ; try (now eapply IHpi ; reflexivity). Qed. Lemma not_bot_bot_ol : forall pax pctr pwk, ~ @ol pax pctr pwk bot bot . Proof. intros pax pctr pwk pi. remember bot as A in pi. rewrite HeqA in pi at 2. remember bot as B in pi. revert HeqA HeqB ; induction pi ; intros HeqA HeqB ; subst ; try (now inversion HeqA) ; try (now apply IHpi ; reflexivity). Qed. (* Lemma 2.4 *) Lemma revert_wedge_ol : forall A B C (pax pctr pwk : formula -> Prop), (forall D E, pax (vee (dual D) (dual E)) \/ pax (wedge D E) -> pax D /\ pax E) -> (forall D E, pctr (wedge D E) -> pctr D /\ pctr E) -> (forall D E, pwk (wedge D E) -> pwk D /\ pwk E) -> @ol pax pctr pwk (wedge A B) C -> @ol pax pctr pwk A C /\ @ol pax pctr pwk B C . Proof with try reflexivity ; try assumption. assert ( forall A B (pax pctr pwk : formula -> Prop), (forall D E, pax (vee (dual D) (dual E)) \/ pax (wedge D E) -> pax D /\ pax E) -> (forall D E, pctr (wedge D E) -> pctr D /\ pctr E) -> (forall D E, pwk (wedge D E) -> pwk D /\ pwk E) -> @ol pax pctr pwk A B -> (forall A1 A2, A = wedge A1 A2 -> @ol pax pctr pwk A1 B /\ @ol pax pctr pwk A2 B) /\ (forall B1 B2, B = wedge B1 B2 -> @ol pax pctr pwk A B1 /\ @ol pax pctr pwk A B2) /\ (forall A1 A2, A = B -> A = wedge A1 A2 -> @ol pax pctr pwk A1 A1 /\ @ol pax pctr pwk A2 A2) ) as Hgen. { intros A B pax pctr pwk Hpax Hpctr Hpwk HI. induction HI ; (split ; [ | split]). - intros A1 A2 HA. apply codual in HA. subst ; simpl. split. + apply ex_ol. apply vee_l_ol. apply ax_ol. destruct (Hpax A1 A2) as [Hpaxl _]... left... + apply ex_ol. apply vee_r_ol. apply ax_ol. destruct (Hpax A1 A2) as [_ Hpaxr]... left... - intros B1 B2 HA. subst ; simpl. split. + apply vee_l_ol. apply ax_ol. destruct (Hpax B1 B2) as [Hpaxl _]... right... + apply vee_r_ol. apply ax_ol. destruct (Hpax B1 B2) as [_ Hpaxr]... right... - intros A1 A2 Hn HA. apply codual in HA. rewrite HA in Hn. simpl in Hn. discriminate Hn. - intros A1 A2 Hn. discriminate Hn. - intros B1 B2 HC. split ; apply top_ol. - intros A1 A2 HC Hn. discriminate Hn. - intros A1 A2 Hw. inversion Hw. subst. split... - intros B1 B2 HC. destruct IHHI1 as [_ [IH1 _]]. destruct IHHI2 as [_ [IH2 _]]. split ; apply wedge_ol. + apply (IH1 B1 B2)... + apply (IH2 B1 B2)... + apply (IH1 B1 B2)... + apply (IH2 B1 B2)... - intros A1 A2 HC Hw. inversion Hw. subst. split. + destruct IHHI1 as [_ [IH1 _]]. apply (IH1 A1 A2)... + destruct IHHI2 as [_ [IH2 _]]. apply (IH2 A1 A2)... - intros A1 A2 Hn. discriminate Hn. - intros B1 B2 HC. destruct IHHI as [_ [IH _]]. split ; apply vee_l_ol ; apply (IH B1 B2)... - intros A1 A2 HC Hn. discriminate Hn. - intros A1 A2 Hn. discriminate Hn. - intros B1 B2 HC. destruct IHHI as [_ [IH _]]. split ; apply vee_r_ol ; apply (IH B1 B2)... - intros A1 A2 HC Hn. discriminate Hn. - intros A1 A2 HA. destruct IHHI as [_ [_ IH]]. split ; apply cw_ol ; try (now constructor) ; try (apply (IH A1 A2)) ; try (apply (Hpctr A1 A2) ; subst)... - intros B1 B2 HB. split ; apply cw_ol ; try (now constructor) ; try (apply (Hpwk B1 B2) ; subst)... - intros A1 A2 HB HA. destruct IHHI as [_ [_ IH]]. apply IH... - intros A1 A2 HB. destruct IHHI as [_ [IH _]]. split ; apply ex_ol ; apply (IH A1 A2)... - intros B1 B2 HA. destruct IHHI as [IH _]. split ; apply ex_ol ; apply (IH B1 B2)... - intros A1 A2 HA HB. destruct IHHI as [_ [_ IH]]. split ; apply (IH A1 A2) ; subst... } intros A B C pax pctr pwk Hpax Hpctr Hpwk Hw. apply Hgen in Hw... destruct Hw as [Hw _]. apply Hw... Qed. (* Basic OL system *) Notation "⊦ A , B" := (@ol (fun _ => True) (fun _ => True) (fun _ => True) A B) (at level 50). (* OL with atomic axioms *) Notation "α⊦ A , B" := (@ol is_var (fun _ => True) (fun _ => True) A B) (at level 50). (* OL with atomic axioms and cw duplication restricted to vee-formulas *) Notation "τ⊦ A , B" := (@ol is_var is_vee (fun _ => True) A B) (at level 50). (* OL with atomic axioms, cw duplication on vee-subformulas and reversed weakening *) Notation "σ⊦ A , B" := (@ol is_var is_vee (fun A => sync A \/ is_covar A) A B) (at level 50). Lemma revert_wedge_ol_basic : forall A B C, ⊦ A ∧ B, C -> ⊦ A, C /\ ⊦ B, C . Proof. intros A B C Hw. apply revert_wedge_ol ; try (now intros ; split ; apply I). assumption. Qed. Lemma ax_var_ol : forall x, ⊦ κ x, ν x . Proof. intro x. change (covar x) with (dual (var x)). apply ax_ol. apply I. Qed. (* Example 2.2 *) Example example_1_3_ol : forall x y, ⊦ bot, vee (vee (wedge (var x) (var y)) (covar x)) (covar y) . Proof. intros x y. apply ex_ol. apply cw_ol ; try now apply I. apply vee_l_ol. apply vee_l_ol. apply wedge_ol ; apply ex_ol. - apply vee_l_ol. apply vee_r_ol. apply ax_var_ol. - apply vee_r_ol. apply ax_var_ol. Qed. (* Proposition 2.3 *) Proposition ax_exp_ol : forall A, α⊦ (dual A), A . Proof with try assumption ; try (apply ex_ol ; assumption). induction A ; try (now simpl ; constructor) ; try (now apply ex_ol ; constructor). - apply ax_ol. apply is_var_var. - rewrite <- bidual. apply ex_ol. apply ax_ol. apply is_var_var. - apply ex_ol. apply wedge_ol ; apply ex_ol. + apply vee_l_ol... + apply vee_r_ol... - apply wedge_ol ; apply ex_ol. + apply vee_l_ol... + apply vee_r_ol... Qed. Lemma atomic_ol : forall A B, ⊦ A, B <-> α⊦ A, B . Proof with try assumption. intros A B. split ; intro H ; induction H ; try now constructor ; assumption. + apply ax_exp_ol. + apply vee_r_ol... + apply ex_ol... + apply ax_ol. apply I. + apply vee_r_ol... + apply ex_ol... Qed. (* Lemma 2.5, Part 1 *) Lemma vee_ctr_ol : forall A B, τ⊦ A, A -> τ⊦ A, B . Proof. induction A ; intros B H. - apply not_var_var_ol in H. contradiction H. - apply not_covar_covar_ol in H. contradiction H. - apply top_ol. - apply not_bot_bot_ol in H. contradiction H. - apply revert_wedge_ol in H. + destruct H as [H1 H2]. { apply wedge_ol. - apply IHA1. apply ex_ol in H1. apply revert_wedge_ol in H1. + apply H1. + intros D E Hv. destruct Hv as [Hv | Hv] ; inversion Hv. + intros D E Hw ; inversion Hw. + intros ; split ; apply I. - apply IHA2. apply ex_ol in H2. apply revert_wedge_ol in H2. + apply H2. + intros D E Hv. destruct Hv as [Hv | Hv] ; inversion Hv. + intros D E Hw ; inversion Hw. + intros ; split ; apply I. } + intros D E Hv. destruct Hv as [Hv | Hv] ; inversion Hv. + intros D E Hw ; inversion Hw. + intros ; split ; apply I. - apply cw_ol ; try now constructor. assumption. Qed. Lemma vee_ol : forall A B, α⊦ A, B <-> τ⊦ A, B . Proof with try assumption. intros A B. split ; intro H ; induction H ; try now constructor... - apply vee_r_ol... - apply vee_ctr_ol... - apply ex_ol... - apply vee_r_ol... - apply ex_ol... Qed. (* Lemma 2.5, Part 2 *) Lemma sync_wk_ol : forall B A, σ⊦ A, A -> is_vee A -> σ⊦ A, B . Proof with try assumption. induction B ; intros A H Hv ; try now (apply cw_ol ; try assumption ; try (left ; constructor) ; try (right ; constructor)). - apply ex_ol. apply top_ol. - apply ex_ol. apply wedge_ol ; apply ex_ol. + apply IHB1... + apply IHB2... Qed. Lemma revert_ol : forall A B, τ⊦ A, B <-> σ⊦ A, B . Proof with try assumption. intros A B. split ; intro H ; induction H ; try now constructor... - apply vee_r_ol... - apply sync_wk_ol... - apply ex_ol... - apply vee_r_ol... - apply ex_ol... Qed. (** First Focused System OLf0 **) Inductive seq_4 : Set := | ll4 | fc4 | rv4 | rr4 . Inductive olf0 : seq_4 -> formula -> formula -> nat -> Prop := (* nat is proof size *) | ax_fc_olf0 : forall x, olf0 fc4 (covar x) (var x) 1 | vee_l_fc_olf0 : forall C A B l1, olf0 fc4 C A l1 -> olf0 fc4 C (vee A B) (S l1) | vee_r_fc_olf0 : forall C A B l1, olf0 fc4 C A l1 -> olf0 fc4 C (vee B A) (S l1) | top_rv_olf0 : forall C, (sync C \/ is_covar C) -> olf0 rv4 C top 1 | top_rr_olf0 : forall C, olf0 rr4 top C 1 | wedge_rv_olf0 : forall C A B l1 l2, olf0 rv4 C A l1 -> olf0 rv4 C B l2 -> olf0 rv4 C (wedge A B) (S (l1+l2)) | wedge_rr_olf0 : forall C A B l1 l2, olf0 rr4 A C l1 -> olf0 rr4 B C l2 -> olf0 rr4 (wedge A B) C (S (l1+l2)) | unfoc_fc_olf0 : forall C A l1, async A -> olf0 rv4 C A l1 -> olf0 fc4 C A (S l1) | unrev_rv_olf0 : forall C A l1, olf0 ll4 C A l1 -> olf0 rv4 C A (S l1) | unrev_rr_olf0 : forall C A l1, olf0 rv4 A C l1 -> olf0 rr4 A C (S l1) | foc_l_ll_olf0 : forall A C l1, sync A -> olf0 fc4 C A l1 -> olf0 ll4 A C (S l1) | foc_r_ll_olf0 : forall A C l1, sync A -> olf0 fc4 C A l1 -> olf0 ll4 C A (S l1) | cw_l_ll_olf0 : forall A C l1, (sync C \/ is_covar C) -> olf0 ll4 A A l1 -> olf0 ll4 A C (S l1) | cw_r_ll_olf0 : forall A C l1, (sync C \/ is_covar C) -> olf0 ll4 A A l1 -> olf0 ll4 C A (S l1) . Notation "l ⊦° A , B ⇑" := (olf0 ll4 A B l) (at level 50). Notation "l ⊦° A ⇓ B" := (olf0 fc4 A B l) (at level 50). Notation "l ⊦° A ⇑ B" := (olf0 rv4 A B l) (at level 50). Notation "l ⊦° ⇑ A , B" := (olf0 rr4 A B l) (at level 50). (* Lemma 3.1 *) Lemma left_is_sync_or_covar_olf0 : forall t C A l, olf0 t C A l -> (t = rv4 -> (sync C \/ is_covar C)) /\ (t = fc4 -> (sync C \/ is_covar C)) /\ (t = ll4 -> (sync C \/ is_covar C) /\ (sync A \/ is_covar A)) . Proof with try reflexivity ; try assumption ; try auto_sync_async. intros t C A l pi. induction pi ; (split ; [ | split]) ; intro eq ; inversion eq ; try (apply IHpi in eq ; auto_sync_async)... - apply IHpi1 in eq... - destruct IHpi as [IH _]. apply IH... - destruct IHpi as [_ [_ IH]]. apply IH... - destruct IHpi as [_ [IH _]]. apply IH... - destruct IHpi as [_ [IH _]]. apply IH... - apply eq. - apply eq. Qed. Lemma left_is_sync_or_covar_fc_olf0 : forall C A l, olf0 fc4 C A l -> sync C \/ is_covar C . Proof. intros C A l pi. apply left_is_sync_or_covar_olf0 in pi. destruct pi as [_ [pi _]]. apply pi. reflexivity. Qed. Lemma left_is_async_or_var_fc_olf0 : forall C A l, olf0 fc4 (dual C) A l -> async C \/ is_var C . Proof. intros C A l pi. apply left_is_sync_or_covar_fc_olf0 in pi. rewrite sync_dual in pi. rewrite is_covar_dual in pi. assumption. Qed. Lemma left_is_sync_or_covar_rv_olf0 : forall C A l, olf0 rv4 C A l -> sync C \/ is_covar C . Proof. intros C A l pi. apply left_is_sync_or_covar_olf0 in pi. destruct pi as [pi _]. apply pi. reflexivity. Qed. Lemma left_is_async_or_var_rv_olf0 : forall C A l, olf0 rv4 (dual C) A l -> async C \/ is_var C . Proof. intros C A l pi. apply left_is_sync_or_covar_rv_olf0 in pi. rewrite sync_dual in pi. rewrite is_covar_dual in pi. assumption. Qed. Lemma left_is_sync_or_covar_ll_olf0 : forall C A l, olf0 ll4 A C l -> sync C \/ is_covar C . Proof. intros C A l pi. apply left_is_sync_or_covar_olf0 in pi. destruct pi as [_ [_ pi]]. apply pi. reflexivity. Qed. Lemma left_is_async_or_var_ll_olf0 : forall C A l, olf0 ll4 A (dual C) l -> async C \/ is_var C . Proof. intros C A l pi. apply left_is_sync_or_covar_ll_olf0 in pi. rewrite sync_dual in pi. rewrite is_covar_dual in pi. assumption. Qed. (* Example 3.2 *) Example example_uniq_olf0 : forall x A B C D, exists l, l ⊦° ⇑ vee (vee (var x) A) B, wedge (vee C (vee D (covar x))) top . Proof with try auto_sync_async. intros x A B C D. eexists. apply unrev_rr_olf0. apply wedge_rv_olf0. - apply unrev_rv_olf0. apply foc_r_ll_olf0... apply vee_r_fc_olf0. apply vee_r_fc_olf0. apply unfoc_fc_olf0... apply unrev_rv_olf0. apply foc_l_ll_olf0... apply vee_l_fc_olf0. apply vee_l_fc_olf0. apply ax_fc_olf0. - apply top_rv_olf0... Qed. (* Example 3.3 *) Example example_1_3_olf0 : forall x y, exists l, l ⊦° ⇑ ⊥, ((ν x ∧ ν y) ∨ κ x) ∨ κ y . Proof with try auto_sync_async. intros x y. eexists. apply unrev_rr_olf0. apply unrev_rv_olf0. apply cw_r_ll_olf0... apply foc_r_ll_olf0... apply vee_l_fc_olf0. apply vee_l_fc_olf0. apply unfoc_fc_olf0... apply wedge_rv_olf0. - apply unrev_rv_olf0. apply foc_l_ll_olf0... apply vee_l_fc_olf0. apply vee_r_fc_olf0. apply unfoc_fc_olf0... apply unrev_rv_olf0. apply foc_l_ll_olf0... apply ax_fc_olf0. - apply unrev_rv_olf0. apply foc_l_ll_olf0... apply vee_r_fc_olf0. apply unfoc_fc_olf0... apply unrev_rv_olf0. apply foc_l_ll_olf0... apply ax_fc_olf0. Qed. (* Proposition 3.4 *) Proposition olf0_to_ol : forall t A B l, olf0 t A B l -> ⊦ A, B . Proof with try assumption ; try (apply ex_ol ; assumption) ; try now constructor. intros t A B l pi. induction pi ; try (now constructor ; assumption) ; try (now apply ex_ol ; constructor ; assumption) ; try (now apply ex_ol ; constructor ; apply ex_ol ; assumption)... - apply ax_var_ol. - apply ex_ol. apply vee_r_ol... - apply ex_ol. apply cw_ol... Qed. (* Lemma 3.5, Fact 1 *) Lemma not_var_var_ll_olf0 : forall x y l, ~ olf0 ll4 (var x) (var y) l . Proof. intros x y l pi. remember (var x) as A. remember (var y) as B. revert x y HeqA HeqB ; induction pi ; intros x0 y0 HeqA HeqB ; subst ; try (now try inversion HeqA ; inversion HeqB) ; try (now eapply IHpi ; reflexivity). Qed. (* Lemma 3.5, Fact 2 *) Lemma not_covar_covar_ll_olf0 : forall x y l, ~ olf0 ll4 (covar x) (covar y) l . Proof. intros x y l pi. remember (covar x) as A. remember (covar y) as B. revert x y HeqA HeqB ; induction pi ; intros x0 y0 HeqA HeqB ; subst ; try (now try inversion HeqA ; inversion HeqB) ; try (now eapply IHpi ; reflexivity). Qed. (* Lemma 3.5, Fact 3 *) Lemma not_bot_bot_ll_olf0 : forall l, ~ olf0 ll4 bot bot l . Proof. intros l pi. remember bot as A in pi. rewrite HeqA in pi at 2. remember bot as B in pi. revert HeqA HeqB ; induction pi ; intros HeqA HeqB ; subst ; try (now try inversion HeqA ; inversion HeqB) ; try (now eapply IHpi ; reflexivity). Qed. (* Lemma 3.5, Fact 4 *) Lemma ex_ll_olf0 : forall C A l, olf0 ll4 C A l -> olf0 ll4 A C l . Proof with try assumption. intros C A l pi. remember ll4 as sk. revert Heqsk ; induction pi ; intros Heqsk ; subst ; try now inversion Heqsk. - apply foc_r_ll_olf0... - apply foc_l_ll_olf0... - apply cw_r_ll_olf0... - apply cw_l_ll_olf0... Qed. (* Lemma 3.5, Fact 5 *) Lemma foc_biform_olf0 : forall A l, olf0 ll4 A A l -> sync A /\ exists l', olf0 fc4 A A l' /\ l' < l . Proof with try assumption. intros A l pi. split. - assert (pi' := pi). apply left_is_sync_or_covar_ll_olf0 in pi. destruct pi... exfalso. inversion H ; subst. apply not_covar_covar_ll_olf0 in pi'... - remember A as B in pi. rewrite HeqB in pi at 1. remember ll4 as sk. revert HeqB Heqsk ; induction pi ; intros HeqB Heqsk ; subst ; try (now inversion Heqsk) ; try (now eexists ; split ; [ eassumption | omega ]) ; try (now apply IHpi in Heqsk ; [ instantiate | reflexivity ] ; destruct IHpi as [l' [Heq IH]] ; eexists ; split ; try eassumption ; try omega). Qed. Lemma uniq_olf0_1 : forall x y z l, ~ l ⊦° vee (vee (var x) (var y)) (var z), vee (vee (var x) (var y)) (var z) ⇑ . Proof. intros x y z l pi. remember (vee (vee (var x) (var y)) (var z)) as A. remember A as B. rewrite HeqB in pi at 1. revert HeqA HeqB ; induction pi ; intros HeqA HeqB ; subst ; try (now inversion HeqA) ; try (now inversion HeqB) ; subst ; try (now (apply IHpi ; reflexivity)). - inversion HeqA ; subst. inversion pi ; subst ; try inversion H2 ; inversion H. - inversion HeqA ; subst. inversion pi ; subst ; try inversion H2 ; inversion H. Qed. Lemma uniq_olf0_2 : forall x u v l, x <> u -> x <> v -> ~ l ⊦° vee (var u) (vee (var v) (covar x)), vee (var u) (vee (var v) (covar x)) ⇑ . Proof. intros x u v l Hu Hv. induction l as [l IH] using (well_founded_induction lt_wf) ; intros pi. inversion pi ; subst ; try (now (apply (IH l1) ; [ omega | assumption ])). - inversion H0 ; subst. + inversion H4 ; inversion H1. + inversion H4 ; subst. * inversion H5 ; inversion H1. * inversion H5 ; subst. inversion H2 ; subst. { inversion H3 ; subst. - inversion H7 ; subst. + inversion H11. * apply Hu ; assumption. * inversion H8. + inversion H11 ; subst. * inversion H12 ; subst. apply Hv ; reflexivity. inversion H8. * inversion H12 ; subst. inversion H9 ; subst. apply not_covar_covar_ll_olf0 in H10. destruct H10. * inversion H8. + inversion H8. - inversion H6. - apply (IH l0) ; [ omega | assumption ]. - apply not_covar_covar_ll_olf0 in H7. destruct H7. } * inversion H1. + inversion H1. - inversion H0 ; subst. + inversion H4 ; inversion H1. + inversion H4 ; subst. * inversion H5 ; inversion H1. * inversion H5 ; subst. inversion H2 ; subst. { inversion H3 ; subst. - inversion H7 ; subst. + inversion H11. * apply Hu ; assumption. * inversion H8. + inversion H11 ; subst. * inversion H12 ; subst. apply Hv ; reflexivity. inversion H8. * inversion H12 ; subst. inversion H9 ; subst. apply not_covar_covar_ll_olf0 in H10. destruct H10. * inversion H8. + inversion H8. - inversion H6. - apply (IH l0) ; [ omega | assumption ]. - apply not_covar_covar_ll_olf0 in H7. destruct H7. } * inversion H1. + inversion H1. Qed. (* Example 3.2 uniqueness *) Example example_uniq_olf0_is_uniq : forall x y z u v l, x <> y -> x <> z -> x <> u -> x <> v -> l ⊦° ⇑ vee (vee (var x) (var y)) (var z), wedge (vee (var u) (vee (var v) (covar x))) top -> l = 13 . Proof with try auto_sync_async. intros x y z u v l Hy Hz Hu Hv pi. inversion pi ; subst. inversion H ; subst. - inversion H4 ; subst. + inversion H2 ; subst. inversion H1 ; subst. * exfalso. { inversion H5 ; subst. - inversion H9 ; subst ; try inversion H10 ; inversion H6. - inversion H9 ; inversion H6. - inversion H6. } * { inversion H5 ; subst. - exfalso. inversion H9 ; inversion H6. - inversion H9 ; subst. + exfalso. inversion H10 ; inversion H6. + inversion H10 ; subst. inversion H7 ; subst. inversion H8 ; subst. * { inversion H12 ; subst. - inversion H16 ; subst. + inversion H17. * reflexivity. * exfalso. inversion H13. + exfalso. inversion H17. * apply Hy ; assumption. * inversion H13. + exfalso. inversion H13. - exfalso. inversion H16. + apply Hz ; assumption. + inversion H13. - exfalso. inversion H13. } * exfalso. inversion H11. * exfalso. apply uniq_olf0_1 in H12. destruct H12. * exfalso. apply not_covar_covar_ll_olf0 in H12. destruct H12. + exfalso. inversion H6. - exfalso. inversion H6. } * exfalso. apply uniq_olf0_1 in H5. destruct H5. * exfalso. apply uniq_olf0_2 in H5 ; assumption. + exfalso. change (⊤) with (dual (⊥)) in H0. apply left_is_async_or_var_ll_olf0 in H0. destruct H0 as [H0 | H0] ; inversion H0. - exfalso. change ((ν u ∨ (ν v ∨ κ x)) ∧ ⊤) with (dual ((κ u ∧ (κ v ∧ ν x)) ∨ ⊥)) in H0. apply left_is_async_or_var_ll_olf0 in H0. destruct H0 as [H0 | H0] ; inversion H0. Qed. (* Cut Elimination *) (* Theorem 3.6, Part 1 *) Lemma cut_elim_v_2_3_olf0 : forall l1, forall x C l2, sync C -> olf0 fc4 (covar x) C l2 -> (forall A, olf0 fc4 (var x) A l1 -> exists l, olf0 fc4 C A l) /\ (forall A, olf0 rv4 (var x) A l1 -> exists l, olf0 rv4 C A l) . Proof with try reflexivity ; try omega ; try eassumption. induction l1 as [l1 IH] using (well_founded_induction lt_wf) ; intros x C l2 Hs pi2 ; split ; intros A pi1 ; inversion pi1 ; subst. - eapply IH in pi2... eapply pi2 in H. destruct H as [l pi]. eexists. apply vee_l_fc_olf0... omega. - eapply IH in pi2... eapply pi2 in H. destruct H as [l pi]. eexists. apply vee_r_fc_olf0... omega. - eapply IH in pi2... destruct pi2 as [_ pi2]. eapply pi2 in H0. destruct H0 as [l pi]. eexists. apply unfoc_fc_olf0... omega. - eexists. apply top_rv_olf0. left... - assert (pi2' := pi2). eapply IH in pi2... destruct pi2 as [_ pi2]. eapply pi2 in H. destruct H as [l' pi']. eapply IH in pi2'... destruct pi2' as [_ pi2']. eapply pi2' in H0. destruct H0 as [l'' pi'']. eexists. apply wedge_rv_olf0... omega. omega. - inversion H. + inversion H1. * eexists. apply unrev_rv_olf0. apply foc_l_ll_olf0... * inversion H2. + eapply IH in pi2... destruct pi2 as [pi2 _]. eapply pi2 in H1. destruct H1 as [l pi]. eexists. apply unrev_rv_olf0... apply foc_r_ll_olf0... omega. + eapply not_var_var_ll_olf0 in H1... + eexists. apply unrev_rv_olf0. apply cw_r_ll_olf0... left... Qed. (* Theorem 3.6, Part 2 *) Lemma cut_elim_v_1_olf0 : forall x A C l1 l2, olf0 ll4 A (var x) l1 -> olf0 ll4 C (covar x) l2 -> exists l, olf0 ll4 A C l . Proof with try reflexivity ; try omega ; try eassumption ; try auto_sync_async. intros x A C l1 l2 pi1 pi2. inversion pi1. - inversion pi2 ; subst. + assert (Hce := cut_elim_v_2_3_olf0 l0 x C l3 H1 H5). destruct Hce as [Hce _]. apply (Hce A) in H0. destruct H0 as [l pi]. eexists. apply foc_l_ll_olf0... + inversion H1. + eexists. apply cw_r_ll_olf0... + eapply not_covar_covar_ll_olf0 in H5... - inversion H0 ; subst. + eexists. apply ex_ll_olf0... + inversion H1. - eexists. apply cw_l_ll_olf0... apply ex_ll_olf0 in pi2. apply left_is_sync_or_covar_ll_olf0 in pi2... - eapply not_var_var_ll_olf0 in H0... Qed. (* Theorem 3.6, Part 3 *) Lemma cut_elim_1_2_3_4_5_olf0 : forall v, forall A B l1, fsize B <= (fst v) -> olf0 rv4 A B l1 -> (forall C, olf0 rv4 C (dual B) (snd v) -> (async B \/ is_var B) -> exists l, olf0 ll4 A C l) /\ (forall C, olf0 ll4 C (dual B) (snd v) -> exists l, olf0 ll4 A C l) /\ (forall C, olf0 fc4 (dual B) C (snd v) -> async B -> exists l, olf0 fc4 A C l) /\ (forall C, olf0 fc4 C (dual B) (snd v) -> (async B \/ is_var B) -> exists l, olf0 ll4 A C l) /\ (forall C, olf0 rv4 (dual B) C (snd v) -> exists l, olf0 rv4 A C l) . Proof with try reflexivity ; try omega ; try eassumption ; try (now unfold lt_nat_nat ; simpl ; left ; omega) ; try (now unfold lt_nat_nat ; simpl ; right ; split ; omega) ; try auto_sync_async ; try (simpl ; try omega ; rewrite fsize_dual ; omega). induction v as [(f,l2) IH] using (well_founded_induction wf_nat_nat) ; intros A B l1 Hsize pi1 ; split ; [ | split ; [ | split ; [ | split ]]] ; intros C pi2 ; inversion pi2 ; subst. (* cut1 *) - intro Hs. apply codual in H ; simpl in H. subst. inversion Hs as [Hs' | Hs'] ; inversion Hs'. - intro Hs. apply codual in H ; simpl in H. subst. inversion Hs as [Hs' | Hs'] ; inversion Hs'. - intro Hs. simpl in H3. apply IH with (f,l0) _ _ _ in pi1... destruct pi1 as [_ [pi1 _]]. apply (pi1 C)... (* cut2 *) - assert (Hs := H0). apply left_is_async_or_var_fc_olf0 in Hs. inversion Hs. + simpl in H4. apply IH with (f,l0) _ _ _ in pi1... destruct pi1 as [_ [_ [pi1 _]]]. apply (pi1 C) in H0... destruct H0 as [l pi]. eexists. apply foc_r_ll_olf0... + inversion H1 ; subst. inversion pi1. eapply cut_elim_v_1_olf0... - simpl in H4. apply left_is_async_or_var_ll_olf0 in pi2. apply IH with (f,l0) _ _ _ in pi1... destruct pi1 as [_ [_ [_ [pi1 _]]]]. apply (pi1 C) in H0... - eexists. apply cw_r_ll_olf0... apply left_is_sync_or_covar_rv_olf0 in pi1... - simpl in H4. assert (pi1' := pi1). apply foc_biform_olf0 in H0. destruct H0 as (Hs & l3 & pi3 & Hl3). rewrite sync_dual in Hs. apply IH with (f,l3) _ _ _ in pi1... destruct pi1 as [_ [_ [pi1 _]]]. apply (pi1 (dual B)) in pi3... destruct pi3 as [l3' pi3]. inversion pi1' ; subst ; simpl in pi2. + apply ex_ll_olf0 in pi2... { inversion pi2 ; subst. - inversion H3 ; inversion H1. - apply IH with (1,l0) _ _ _ in pi1'... + destruct pi1' as [_ [_ [pi1' _]]]. apply (pi1' C) in H3... destruct H3 as [l4 pi4]. eexists. apply foc_r_ll_olf0... + unfold lt_nat_nat ; simpl in Hsize ; simpl... - apply not_bot_bot_ll_olf0 in H3 ; destruct H3. - eexists. apply cw_r_ll_olf0... } + simpl in Hsize. inversion pi3 ; subst. * assert (Has := sync_or_async A0). inversion Has. { rewrite <- bidual in H2. inversion H5 ; subst ; try (now rewrite <- H3 in H2 ; simpl in H2 ; inversion H2). apply IH with (fsize A0,l4) _ _ _ in H4... destruct H4 as [pi4 _]. rewrite bidual in pi4. apply (pi4 A) in H0... destruct H0 as [l6 pi6]. eexists. apply cw_l_ll_olf0... } { apply IH with (fsize A0,l1) _ _ _ in H0... destruct H0 as [_ [_ [_ [pi4 _]]]]. apply (pi4 A) in H5... destruct H5 as [l6 pi6]. eexists. apply cw_l_ll_olf0... } * assert (Has := sync_or_async B0). inversion Has. { rewrite <- bidual in H2. inversion H5 ; subst ; try (now rewrite <- H3 in H2 ; simpl in H2 ; inversion H2). apply IH with (fsize B0,l5) _ _ _ in H4... destruct H4 as [pi4 _]. rewrite bidual in pi4. apply (pi4 A) in H1... destruct H1 as [l6 pi6]. eexists. apply cw_l_ll_olf0... } { apply IH with (fsize B0,l1) _ _ _ in H1... destruct H1 as [_ [_ [_ [pi4 _]]]]. apply (pi4 A) in H5... destruct H5 as [l6 pi6]. eexists. apply cw_l_ll_olf0... } * inversion H2. + assert (H1 := H0). apply left_is_sync_or_covar_ll_olf0 in H1. inversion H1. * destruct B ; try (now inversion Hs) ; inversion H2. * inversion H2 ; subst. eapply cut_elim_v_1_olf0 in pi2... destruct pi2 as [l pi2]. eexists. apply ex_ll_olf0... (* cut3 *) - intro Ha. apply codual in H. subst ; simpl in Ha. inversion Ha. - intro Ha. simpl in H3. apply IH with (f,l0) _ _ _ in pi1... destruct pi1 as [_ [_ [pi1 _]]]. apply (pi1 A0) in H... destruct H as [l pi]. eexists. apply vee_l_fc_olf0... - intro Ha. simpl in H3. apply IH with (f,l0) _ _ _ in pi1... destruct pi1 as [_ [_ [pi1 _]]]. apply (pi1 A0) in H... destruct H as [l pi]. eexists. apply vee_r_fc_olf0... - intro Ha. simpl in H4. apply IH with (f,l0) _ _ _ in pi1... destruct pi1 as [_ [_ [_ [_ pi1]]]]. apply (pi1 C) in H0... destruct H0 as [l pi]. eexists. apply unfoc_fc_olf0... (* cut4 *) - intro Hs. apply codual in H. subst. inversion pi1. eexists... - intro Hs. apply codual in H. subst. inversion pi1 ; subst. + simpl in H3. simpl in Hsize ; rewrite fsize_dual in Hsize. assert (Has := sync_or_async A0). inversion Has. { apply IH with (fsize A0,l0) _ _ _ in H2... destruct H2 as [_ [_ [_ [pi4 _]]]]. rewrite bidual in pi4. apply (pi4 C) in H0... } { inversion H0 ; subst ; try now inversion H. apply IH with (fsize A0,l3) _ _ _ in H4... destruct H4 as [pi4 _]. apply (pi4 A) in H2... destruct H2 as [l6 pi6]. eexists. apply ex_ll_olf0... } + apply left_is_sync_or_covar_ll_olf0 in H. inversion H as [Hs2 | Hs2] ; inversion Hs2. - intro Hs. apply codual in H. subst. inversion pi1 ; subst. + simpl in H3. simpl in Hsize ; rewrite !fsize_dual in Hsize. assert (Has := sync_or_async A0). inversion Has. { apply IH with (fsize A0,l0) _ _ _ in H5... destruct H5 as [_ [_ [_ [pi4 _]]]]. rewrite bidual in pi4. apply (pi4 C) in H0... } { inversion H0 ; subst ; try now inversion H. apply IH with (fsize A0,l4) _ _ _ in H4... destruct H4 as [pi4 _]. apply (pi4 A) in H5... destruct H5 as [l6 pi6]. eexists. apply ex_ll_olf0... } + apply left_is_sync_or_covar_ll_olf0 in H. inversion H as [Hs2 | Hs2] ; inversion Hs2. - intro Hs. inversion Hs. + inversion H ; destruct B ; try (now inversion H1) ; inversion H. + inversion H1 ; subst. simpl in pi2. inversion pi2 ; subst. inversion H3. inversion pi1. eapply cut_elim_v_1_olf0... (* cut5 *) - eexists. apply top_rv_olf0. apply left_is_sync_or_covar_rv_olf0 in pi1... - simpl in H4. assert (Hs := H0). apply left_is_async_or_var_rv_olf0 in Hs. assert (pi1' := pi1). apply IH with (f,l0) _ _ _ in pi1... destruct pi1 as [_ [_ [_ [_ pi1]]]]. apply (pi1 A0) in H... destruct H as [l4 pi4]. apply IH with (f,l3) _ _ _ in pi1'... destruct pi1' as [_ [_ [_ [_ pi1']]]]. apply (pi1' B0) in H0... destruct H0 as [l5 pi5]. eexists. apply wedge_rv_olf0... - assert (Hs := pi2). apply left_is_async_or_var_rv_olf0 in Hs. inversion pi2 ; subst. + apply left_is_sync_or_covar_ll_olf0 in H. inversion H as [Hs2 | Hs2] ; inversion Hs2. + apply left_is_sync_or_covar_ll_olf0 in H. inversion H as [Hs2 | Hs2] ; inversion Hs2. + simpl in H5. apply ex_ll_olf0 in H0... apply IH with (f,l3) _ _ _ in pi1... destruct pi1 as [_ [pi1 _]]. apply (pi1 C) in H0... destruct H0 as [l pi]. eexists. apply unrev_rv_olf0... Qed. (* Theorem 3.6, Part 4 *) Lemma cut_elim_00_olf0 : forall A B C l1 l2, olf0 rr4 A B l1 -> olf0 rv4 C (dual B) l2 -> exists l, olf0 rv4 C A l . Proof with try reflexivity ; try eassumption ; try auto_sync_async ; try omega. intros A B C l1 l2 pi1. remember rr4 as sk. revert Heqsk ; induction pi1 ; intros Heqsk ; subst ; try inversion Heqsk ; simpl ; intro pi2. - eexists. apply top_rv_olf0. apply left_is_sync_or_covar_rv_olf0 in pi2... - assert (pi2_2 := pi2). apply IHpi1_1 in pi2... apply IHpi1_2 in pi2_2... destruct pi2 as [l3 pi3]. destruct pi2_2 as [l4 pi4]. eexists. apply wedge_rv_olf0... - assert (Hs := sync_or_async C0). inversion Hs. + apply cut_elim_1_2_3_4_5_olf0 with (fsize (dual C0),l1) _ _ _ in pi2... destruct pi2 as [pi2 _]. rewrite bidual in pi2. apply (pi2 _) in pi1... destruct pi1 as [l pi]. eexists. apply unrev_rv_olf0... + apply cut_elim_1_2_3_4_5_olf0 with (fsize C0,l2) _ _ _ in pi1... destruct pi1 as [pi1 _]. apply (pi1 _) in pi2... destruct pi2 as [l pi]. apply ex_ll_olf0 in pi... eexists. apply unrev_rv_olf0... Qed. (* Theorem 3.6, Part 5 *) Lemma cut_elim_0_olf0 : forall A B C l1 l2, olf0 rr4 A B l1 -> olf0 rr4 C (dual B) l2 -> exists l, olf0 rr4 A C l . Proof with try reflexivity ; try eassumption. intros A B C l1 l2 pi1. remember rr4 as sk. revert Heqsk ; induction pi1 ; intros Heqsk ; subst ; try inversion Heqsk ; simpl ; intro pi2. - eexists. apply top_rr_olf0. - assert (pi2_2 := pi2). apply IHpi1_1 in pi2... apply IHpi1_2 in pi2_2... destruct pi2 as [l3 pi3]. destruct pi2_2 as [l4 pi4]. eexists. apply wedge_rr_olf0... - eapply cut_elim_00_olf0 in pi2. + destruct pi2 as [l pi]. eexists. apply unrev_rr_olf0... + rewrite bidual... Qed. (* Completeness of OLf0 wrt OL *) (* Lemma 3.7, Fact 1 *) Lemma top_r_rr_olf0 : forall C, exists l, olf0 rr4 C top l . Proof with try auto_sync_async. induction C. - eexists. apply unrev_rr_olf0. apply top_rv_olf0... - eexists. apply unrev_rr_olf0. apply top_rv_olf0... - eexists. apply top_rr_olf0. - eexists. apply unrev_rr_olf0. apply top_rv_olf0... - destruct IHC1 as [l1 IHC1]. destruct IHC2 as [l2 IHC2]. eexists. apply wedge_rr_olf0 ; eassumption. - destruct IHC1 as [l1 IHC1]. eexists. apply unrev_rr_olf0. apply top_rv_olf0... Qed. (* Lemma 3.7, Fact 2 *) Lemma wedge_r_rr_olf0 : forall C A B l1 l2, olf0 rr4 C A l1 -> olf0 rr4 C B l2 -> exists l, olf0 rr4 C (wedge A B) l . Proof with try eassumption. induction C ; intros A B l1 l2 pi1 pi2. - inversion pi1. inversion pi2. eexists. apply unrev_rr_olf0. apply wedge_rv_olf0... - inversion pi1. inversion pi2. eexists. apply unrev_rr_olf0. apply wedge_rv_olf0... - eexists. apply top_rr_olf0. - inversion pi1. inversion pi2. eexists. apply unrev_rr_olf0. apply wedge_rv_olf0... - inversion pi1. + inversion pi2. * subst. eapply IHC1 in H7. destruct H7 as [l1' IH1]. eapply IHC2 in H8. destruct H8 as [l2' IH2]. eexists. apply wedge_rr_olf0 ; eassumption. eassumption. eassumption. * apply left_is_sync_or_covar_rv_olf0 in H5. inversion H5 as [Hs | Hs] ; inversion Hs. + apply left_is_sync_or_covar_rv_olf0 in H. inversion H as [Hs | Hs] ; inversion Hs. - inversion pi1. inversion pi2. eexists. apply unrev_rr_olf0. apply wedge_rv_olf0... Qed. (* Lemma 3.7, Fact 3 *) Lemma unrev_l_rr_olf0 : forall C A l, olf0 rv4 A C l -> exists l', olf0 rr4 C A l' . Proof with try reflexivity ; try eassumption. induction C ; intros A l pi. - inversion pi. apply ex_ll_olf0 in H... eexists. apply unrev_rr_olf0. apply unrev_rv_olf0... - inversion pi. apply ex_ll_olf0 in H... eexists. apply unrev_rr_olf0. apply unrev_rv_olf0... - eexists. apply top_rr_olf0. - inversion pi. apply ex_ll_olf0 in H... eexists. apply unrev_rr_olf0. apply unrev_rv_olf0... - inversion pi ; subst. + apply IHC1 in H1. destruct H1 as [l1' H1]. apply IHC2 in H3. destruct H3 as [l2' H2]. eexists. eapply wedge_rr_olf0... + apply left_is_sync_or_covar_ll_olf0 in H. inversion H as [Hs | Hs] ; inversion Hs. - inversion pi. apply ex_ll_olf0 in H... eexists. apply unrev_rr_olf0. apply unrev_rv_olf0... Qed. (* Lemma 3.7, Fact 4 *) Lemma ex_rr_olf0 : forall A C l, olf0 rr4 A C l -> exists l', olf0 rr4 C A l' . Proof with try eassumption. intros A C l pi. remember rr4 as sk. revert Heqsk ; induction pi ; intros Heqsk ; subst ; try inversion Heqsk. - apply top_r_rr_olf0. - assert (Heqsk2 := Heqsk). apply IHpi1 in Heqsk. destruct Heqsk as [l1' IH1]. apply IHpi2 in Heqsk2. destruct Heqsk2 as [l2' IH2]. eapply wedge_r_rr_olf0... - eapply unrev_l_rr_olf0... Qed. (* Lemma 3.8, Part 1 *) Lemma vee_l_async_olf0 : forall l A B C, olf0 rv4 C A l -> async A -> (exists l', olf0 rv4 (vee A B) C l') /\ (exists l', olf0 rv4 (vee B A) C l') . Proof with try auto_sync_async. intros l A B C Hasync pi. split ; eexists. - apply unrev_rv_olf0. apply foc_l_ll_olf0... apply vee_l_fc_olf0. apply unfoc_fc_olf0... eassumption. - apply unrev_rv_olf0. apply foc_l_ll_olf0... apply vee_r_fc_olf0. apply unfoc_fc_olf0... eassumption. Qed. (* Lemma 3.8, Part 2 *) Lemma vee_l_sync_olf0 : forall l t A C B, olf0 t A C l -> t <> rr4 -> sync A -> (exists l', olf0 t (vee A B) C l') /\ (exists l', olf0 t (vee B A) C l') . Proof with try reflexivity ; try assumption ; try omega ; try auto_sync_async. induction l using (well_founded_induction lt_wf) ; intros t A C B pi Ht Hsync. inversion pi ; subst ; try (now destruct Ht ; reflexivity). - inversion Hsync. - eapply H with l1 _ _ _ _ in Ht... + destruct Ht as [[l1' IH1] [l2' IH2]]. split ; eexists ; apply vee_l_fc_olf0. * apply IH1. * apply IH2. + assumption. + assumption. - eapply H with l1 _ _ _ _ in Ht... + destruct Ht as [[l1' IH1] [l2' IH2]]. split ; eexists ; apply vee_r_fc_olf0. * apply IH1. * apply IH2. + assumption. + assumption. - split ; eexists ; apply top_rv_olf0... - assert (Ht2 := Ht). eapply H with l1 _ _ _ _ in Ht... + destruct Ht as [[l1' IH11] [l2' IH12]]. eapply H with l2 _ _ _ _ in Ht2... * destruct Ht2 as [[l1'' IH21] [l2'' IH22]]. split ; eexists ; apply wedge_rv_olf0... exact IH11. exact IH21. exact IH12. exact IH22. * assumption. * assumption. + assumption. + assumption. - assert (rv4 <> rr4) as Ht2. intro He ; inversion He. eapply H with l1 _ _ _ _ in Ht2... + destruct Ht2 as [[l1' IH1] [l2' IH2]]. split ; eexists ; apply unfoc_fc_olf0... * exact IH1. * exact IH2. + assumption. + assumption. - assert (ll4 <> rr4) as Ht2. intro He ; inversion He. eapply H with l1 _ _ _ _ in Ht2... + destruct Ht2 as [[l1' IH1] [l2' IH2]]. split ; eexists ; apply unrev_rv_olf0... * exact IH1. * exact IH2. + assumption. + assumption. - split ; eexists ; apply foc_l_ll_olf0... apply vee_l_fc_olf0 ; eassumption. apply vee_r_fc_olf0 ; eassumption. - assert (HA := pi). apply ex_ll_olf0 in HA. apply left_is_sync_or_covar_ll_olf0 in HA. destruct HA. + assert (fc4 <> rr4) as Ht2. intro He ; inversion He. eapply H with l1 _ _ _ _ in Ht2... * destruct Ht2 as [[l1' IH1] [l2' IH2]]. split ; eexists ; apply foc_r_ll_olf0... exact IH1. exact IH2. * assumption. * assumption. + inversion H2 ; subst. split ; eexists ; apply foc_l_ll_olf0... * apply vee_l_fc_olf0. apply unfoc_fc_olf0... apply unrev_rv_olf0. apply foc_l_ll_olf0... eassumption. * apply vee_r_fc_olf0. apply unfoc_fc_olf0... apply unrev_rv_olf0. apply foc_l_ll_olf0... eassumption. - apply foc_biform_olf0 in H1. destruct H1 as (Hs & l1' & pi' & Hleq). assert (fc4 <> rr4) as Ht2 by (intro He ; inversion He). eapply H in pi'... destruct pi' as [[l1'' IH1] [l2'' IH2]]. split ; eexists ; apply cw_l_ll_olf0... + apply foc_r_ll_olf0... apply vee_l_fc_olf0. exact IH1. + apply foc_r_ll_olf0... apply vee_r_fc_olf0. exact IH2. - split ; eexists ; apply cw_r_ll_olf0... + eassumption. + eassumption. Qed. (* Proposition 3.9 *) Proposition ax_exp_rv_olf0 : forall s, forall A, fsize A = s -> (sync A \/ is_covar A) -> exists l, olf0 rv4 A (dual A) l . Proof with try reflexivity ; try (simpl ; omega) ; try eassumption ; try auto_sync_async. induction s as [s IH] using (well_founded_induction lt_wf) ; intros A Hsize Hs. inversion Hs as [Hs' | Hs'] ; inversion Hs' ; subst. - eexists. apply unrev_rv_olf0. apply foc_l_ll_olf0... apply ax_fc_olf0. - eexists. apply top_rv_olf0... - assert (Hsa1 := sync_or_async A0). assert (Hsa2 := sync_or_async B). destruct Hsa1 as [Hsa1 | Hsa1]. { assert (sync A0 \/ is_covar A0) as HA1... apply IH with (fsize A0) _ in HA1... destruct HA1 as [l1 HA1]. apply vee_l_sync_olf0 with _ _ _ _ B in HA1... destruct HA1 as [[l1' HA1] _]. destruct Hsa2 as [Hsa2 | Hsa2]. - assert (sync B \/ is_covar B) as HA2... apply IH with (fsize B) _ in HA2... destruct HA2 as [l2 HA2]. apply vee_l_sync_olf0 with _ _ _ _ A0 in HA2... + destruct HA2 as [_ [l2' HA2]]. eexists. simpl. apply wedge_rv_olf0... + intro Heq ; inversion Heq. - assert (sync (dual B) \/ is_covar (dual B)) as HA2... apply IH with (fsize B) _ in HA2... + destruct HA2 as [l2 HA2]. rewrite bidual in HA2. eexists. simpl. apply wedge_rv_olf0... apply unrev_rv_olf0. apply foc_l_ll_olf0... apply vee_r_fc_olf0. apply unfoc_fc_olf0... + apply fsize_dual. - intro Heq ; inversion Heq. } { assert (sync (dual A0) \/ is_covar (dual A0)) as HA1... apply IH with (fsize A0) _ in HA1... destruct HA1 as [l1 HA1]. rewrite bidual in HA1. destruct Hsa2 as [Hsa2 | Hsa2]. - assert (sync B \/ is_covar B) as HA2... apply IH with (fsize B) _ in HA2... destruct HA2 as [l2 HA2]. apply vee_l_sync_olf0 with _ _ _ _ A0 in HA2... + destruct HA2 as [_ [l2' HA2]]. apply vee_l_async_olf0 with _ _ B _ in HA1... destruct HA1 as [[l' HA1] _]... eexists. simpl. apply wedge_rv_olf0... + intro Heq ; inversion Heq. - assert (sync (dual B) \/ is_covar (dual B)) as HA2... apply IH with (fsize B) _ in HA2... + destruct HA2 as [l2 HA2]. rewrite bidual in HA2. apply vee_l_async_olf0 with _ _ B _ in HA1... destruct HA1 as [[l' HA1] _]... apply vee_l_async_olf0 with _ _ A0 _ in HA2... destruct HA2 as [_ [l'' HA2]]... eexists. simpl. apply wedge_rv_olf0... + apply fsize_dual. - apply fsize_dual. } - eexists. apply unrev_rv_olf0. apply foc_r_ll_olf0... apply ax_fc_olf0. Qed. (* Theorem 3.10 *) Theorem ol_to_olf0 : forall A B, σ⊦ A, B -> exists l, olf0 rr4 A B l . Proof with try reflexivity ; try eassumption ; try auto_sync_async. intros A B pi. induction pi. - inversion H ; subst. eexists. apply unrev_rr_olf0. apply unrev_rv_olf0. apply foc_r_ll_olf0... apply ax_fc_olf0. - eexists. apply top_rr_olf0. - destruct IHpi1 as [l1' pi1']. destruct IHpi2 as [l2' pi2']. eexists. apply wedge_rr_olf0... - destruct IHpi as [l' pi']. assert (exists l0, olf0 rv4 (vee A B) (dual A) l0). + assert (Hs := sync_or_async A). inversion Hs as [Hs1 | Hs1]. * assert (Hax := ax_exp_rv_olf0 (fsize A) A). assert (sync A \/ is_covar A) as Hs2... apply Hax in Hs2... destruct Hs2 as [l2 pi2]. eapply (vee_l_sync_olf0 _ _ A)... intro Heq ; inversion Heq. * assert (Hax := ax_exp_rv_olf0 (fsize (dual A)) (dual A)). rewrite bidual in Hax. assert (sync (dual A) \/ is_covar (dual A)) as Hs2... apply Hax in Hs2... destruct Hs2 as [l2 pi2]. eapply (vee_l_async_olf0 _ A _ _)... + destruct H as [l3 pi3]. apply ex_rr_olf0 in pi'. destruct pi' as [l4 pi']. eapply cut_elim_00_olf0 in pi3... destruct pi3 as [l5 pi3]. eexists. eapply unrev_rr_olf0... - destruct IHpi as [l' pi']. assert (exists l0, olf0 rv4 (vee B A) (dual A) l0). + assert (Hs := sync_or_async A). inversion Hs. * assert (Hax := ax_exp_rv_olf0 (fsize A) A). assert (sync A \/ is_covar A) as Hs2... apply Hax in Hs2... destruct Hs2 as [l2 pi2]. eapply (vee_l_sync_olf0 _ _ A)... intro Heq ; inversion Heq. * assert (Hax := ax_exp_rv_olf0 (fsize (dual A)) (dual A)). rewrite bidual in Hax. assert (sync (dual A) \/ is_covar (dual A)) as Hs2... apply Hax in Hs2... destruct Hs2 as [l2 pi2]. eapply (vee_l_async_olf0 _ A _ _) ... + destruct H as [l3 pi3]. apply ex_rr_olf0 in pi'. destruct pi' as [l4 pi']. eapply cut_elim_00_olf0 in pi3... destruct pi3 as [l5 pi3]. eexists. apply unrev_rr_olf0... - destruct IHpi as [l' pi']. inversion pi' ; subst ; try now inversion H. inversion H1 ; subst ; try now inversion H. eexists. apply unrev_rr_olf0. apply unrev_rv_olf0. apply cw_l_ll_olf0... - destruct IHpi as [l' pi']. eapply ex_rr_olf0... Qed. (* Proposition 3.11 *) Proposition cut_elim_ol : forall A B C, ⊦ A, B -> ⊦ dual B, C -> ⊦ A, C . Proof with try eassumption. intros A B C pi1 pi2. apply atomic_ol in pi1. apply vee_ol in pi1. apply revert_ol in pi1. apply ol_to_olf0 in pi1. destruct pi1 as [l1 pi1]. apply atomic_ol in pi2. apply vee_ol in pi2. apply revert_ol in pi2. apply ol_to_olf0 in pi2. destruct pi2 as [l2 pi2]. apply ex_rr_olf0 in pi2. destruct pi2 as [l2' pi2]. eapply cut_elim_0_olf0 in pi1... destruct pi1 as [l1' pi1]. eapply olf0_to_ol... Qed. (** Soundness and Completeness of OL wrt Ortholattices **) (* Soundness of OL *) (* with ⊦ A, B := leq (perp A) B *) (* embedding of formulas into an ortholattice *) Fixpoint f2o {T leq} {IL : PreInvolLattice leq} r A : T := match A with | var x => r x | covar x => perp (r x) | top => te | bot => be | wedge A B => inf (f2o r A) (f2o r B) | vee A B => sup (f2o r A) (f2o r B) end. Lemma dual_top_valid {T leq} {IL : PreInvolLattice (T:=T) leq} : leq (perp te) be /\ leq be (perp te) . Proof. split. - eapply PreOrder_Transitive. + apply contrap. apply te_geq. + apply invol_leq. - apply be_leq. Qed. Lemma dual_bot_valid {T leq} {IL : PreInvolLattice (T:=T) leq} : leq (perp be) te /\ leq te (perp be) . Proof. split. - apply te_geq. - eapply PreOrder_Transitive. + apply invol_geq. + apply contrap. apply be_leq. Qed. Lemma dual_wedge_valid {T leq} {IL : PreInvolLattice (T:=T) leq} : forall x y, leq (perp (inf x y)) (sup (perp x) (perp y)) /\ leq (sup (perp x) (perp y)) (perp (inf x y)) . Proof. split. - eapply PreOrder_Transitive. + apply contrap. apply inf_geq. * eapply PreOrder_Transitive. apply contrap. apply sup_geq1. apply invol_leq. * eapply PreOrder_Transitive. apply contrap. apply sup_geq2. apply invol_leq. + apply invol_leq. - apply sup_leq. + apply contrap. apply inf_leq1. + apply contrap. apply inf_leq2. Qed. Lemma dual_vee_valid {T leq} {IL : PreInvolLattice (T:=T) leq} : forall x y, leq (perp (sup x y)) (inf (perp x) (perp y)) /\ leq (inf (perp x) (perp y)) (perp (sup x y)) . Proof. split. - apply inf_geq. + apply contrap. apply sup_geq1. + apply contrap. apply sup_geq2. - eapply PreOrder_Transitive. + apply invol_geq. + apply contrap. apply sup_leq. * eapply PreOrder_Transitive. apply invol_geq. apply contrap. apply inf_leq1. * eapply PreOrder_Transitive. apply invol_geq. apply contrap. apply inf_leq2. Qed. Lemma f2o_dual {T leq} {IL : PreInvolLattice (T:=T) leq} : forall r A, leq (perp (f2o r A)) (f2o r (dual A)) /\ leq (f2o r (dual A)) (perp (f2o r A)) . Proof. induction A ; simpl. - split ; apply PreOrder_Reflexive. - split. + apply invol_leq. + apply invol_geq. - apply dual_top_valid. - apply dual_bot_valid. - destruct IHA1. destruct IHA2. split. + eapply PreOrder_Transitive. * apply (proj1 (dual_wedge_valid _ _)). * apply sup_leq. eapply PreOrder_Transitive. apply H. apply sup_geq1. eapply PreOrder_Transitive. apply H1. apply sup_geq2. + assert (leq (sup (perp (f2o r A1)) (perp (f2o r A2))) (perp (inf (f2o r A1) (f2o r A2)))) by apply (proj2 (dual_wedge_valid _ _ )). apply sup_leq. eapply PreOrder_Transitive. apply H0. apply contrap. apply inf_leq1. eapply PreOrder_Transitive. apply H2. apply contrap. apply inf_leq2. - destruct IHA1. destruct IHA2. split. + eapply PreOrder_Transitive. apply (proj1 (dual_vee_valid _ _)). apply inf_geq. * eapply PreOrder_Transitive. apply inf_leq1. assumption. * eapply PreOrder_Transitive. apply inf_leq2. assumption. + assert (leq (inf (perp (f2o r A1)) (perp (f2o r A2))) (perp (sup (f2o r A1) (f2o r A2)))) by apply (proj2 (dual_vee_valid _ _)). eapply PreOrder_Transitive ; try eassumption. apply inf_geq. eapply PreOrder_Transitive. apply inf_leq1. assumption. eapply PreOrder_Transitive. apply inf_leq2. assumption. Qed. Lemma ex_valid {T leq} {IL : PreInvolLattice (T:=T) leq} : forall A B, leq (perp A) B -> leq (perp B) A . Proof. intros A B pi. apply PreOrder_Transitive with (perp (perp A)). - apply contrap. assumption. - apply invol_leq. Qed. Lemma top_valid {T leq} {IL : PreInvolLattice (T:=T) leq} : forall A, leq (perp te) A . Proof. intros. eapply PreOrder_Transitive. - apply (proj1 dual_top_valid). - apply be_leq. Qed. Lemma wedge_valid {T leq} {IL : PreInvolLattice (T:=T) leq} : forall A B C, leq (perp A) C -> leq (perp B) C -> leq (perp (inf A B)) C . Proof. intros A B C pi1 pi2. apply contrap. eapply PreOrder_Transitive ; [ | apply invol_geq]. apply inf_geq ; apply ex_valid ; assumption. Qed. Lemma vee_l_valid {T leq} {IL : PreInvolLattice (T:=T) leq} : forall A C B, leq (perp A) C -> leq (perp (sup A B)) C . Proof. intros A C B pi. eapply PreOrder_Transitive. - apply contrap. apply sup_geq1. - assumption. Qed. Lemma vee_r_valid {T leq} {IL : PreInvolLattice (T:=T) leq} : forall A C B, leq (perp A) C -> leq (perp (sup B A)) C . Proof. intros A C B pi. eapply PreOrder_Transitive. - apply contrap. apply sup_geq2. - assumption. Qed. Lemma cw_valid {T leq} {OL : PreOrthoLattice (T:=T) leq} : forall A B, leq (perp A) A -> leq (perp A) B . Proof. intros A B pi. apply PreOrder_Transitive with (inf A (perp A)). - apply inf_geq. + assumption. + apply PreOrder_Reflexive. - eapply PreOrder_Transitive. + apply contrap. eapply PreOrder_Transitive. * apply (proj1 dual_bot_valid). * eapply PreOrder_Transitive. apply compl. apply (proj2 (dual_wedge_valid _ _)). + apply be_leq. Qed. (* Theorem 2.1 o Theorem 1.6, Part 1 *) Theorem ol_to_ord {T leq} {OL : PreOrthoLattice (T:=T) leq} : forall r A B, ⊦ A, B -> leq (perp (f2o r A)) (f2o r B) . Proof with try assumption. intros r A B pi. induction pi. - assert (Hd := f2o_dual r (dual A)). destruct Hd as [Hd _]. rewrite bidual in Hd... - apply top_valid. - apply wedge_valid... - apply vee_l_valid... - apply vee_r_valid... - apply cw_valid... - apply ex_valid... Qed. (* Completeness of OL *) (* with leq A B := ⊦ dual A, B *) (* the order structure on formulas *) Definition OL_leq := fun A B => ⊦ dual A, B . Instance OL_refl : Reflexive OL_leq. Proof. intro A. apply ax_ol. apply I. Qed. Instance OL_trans : Transitive OL_leq. Proof. intros A B C pi1 pi2. eapply cut_elim_ol ; eassumption. Qed. Instance OL_PreOrder : PreOrder OL_leq. Proof. split. - apply OL_refl. - apply OL_trans. Defined. Instance OL_PreLattice : PreLattice OL_leq. Proof with try (now apply I) ; try assumption. split with vee wedge top bot ; try (intros A B C) ; try (intros A B) ; try intro A. - apply OL_PreOrder. - apply ex_ol. apply vee_l_ol. apply ex_ol. apply ax_ol... - apply ex_ol. apply vee_r_ol. apply ex_ol. apply ax_ol... - intros pi1 pi2. apply wedge_ol... - apply vee_l_ol. apply ax_ol... - apply vee_r_ol. apply ax_ol... - intros pi1 pi2. apply ex_ol. apply wedge_ol ; apply ex_ol... - apply ex_ol. apply top_ol. - apply top_ol. Defined. Lemma OL_leq_dec : forall A B, OL_leq A B -> OL_leq (dual B) (dual A) . Proof. intros A B H. apply ex_ol. rewrite bidual. assumption. Qed. Instance OL_InvolLattice : PreInvolLattice OL_leq. Proof. split with dual. - apply OL_PreLattice. - intro A. rewrite bidual. reflexivity. - intro A. rewrite bidual. reflexivity. - intros A B. split. + intro pi. apply ex_ol. unfold OL_leq in pi. simpl in pi. rewrite bidual in pi. assumption. + apply OL_leq_dec. Defined. Instance OL_OrthoLattice : PreOrthoLattice OL_leq. Proof with try now apply I. split with OL_InvolLattice. intro A. apply ex_ol. apply cw_ol... apply vee_l_ol. apply ex_ol. apply vee_r_ol. apply ax_ol... Defined. (* Theorem 2.1 o Theorem 1.6, Part 2 *) Theorem ord_to_ol : forall A B, (forall leq, forall OL : PreOrthoLattice (T:=formula) leq, leq A B) -> ⊦ dual A, B . Proof. intros A B Ho. apply Ho. apply OL_OrthoLattice. Qed. Definition OL_equiv := fun A B => OL_leq A B /\ OL_leq B A . Notation "A ≡ B" := (OL_equiv A B) (at level 30). Instance OL_equiv_refl : Reflexive OL_equiv. Proof. split ; apply OL_refl. Qed. Instance OL_equiv_sym : Symmetric OL_equiv. Proof. split ; unfold OL_equiv in H ; destruct H as [H1 H2] ; assumption. Qed. Instance OL_Equiv : Equivalence OL_equiv. Proof. split. - apply OL_equiv_refl. - apply OL_equiv_sym. - split ; unfold OL_equiv in H ; unfold OL_equiv in H0 ; destruct H as [H1 H2] ; destruct H0 as [H3 H4] ; eapply OL_trans ; eassumption. Qed. Instance OL_equiv_compat : Proper (OL_equiv ==> OL_equiv ==> iff) OL_leq. Proof with try assumption. intros x y [Hxy Hyx] x' y' [Hxy' Hyx']. split. - intro Hxx. transitivity x... transitivity x'... - intro Hyy. transitivity y... transitivity y'... Qed. Instance OL_dual_compat : Proper (OL_equiv ==> OL_equiv) dual. Proof. intros x y [Hxy Hyx]. split ; apply ex_ol ; rewrite bidual ; assumption. Qed. Instance OL_wedge_compat : Proper (OL_equiv ==> OL_equiv ==> OL_equiv) wedge. Proof with try assumption. intros x y [Hxy Hyx] x' y' [Hxy' Hyx']. split. - apply ex_ol. apply wedge_ol. + apply ex_ol. apply vee_l_ol... + apply ex_ol. apply vee_r_ol... - apply ex_ol. apply wedge_ol. + apply ex_ol. apply vee_l_ol... + apply ex_ol. apply vee_r_ol... Qed. Instance OL_vee_compat : Proper (OL_equiv ==> OL_equiv ==> OL_equiv) vee. Proof with try assumption. intros x y [Hxy Hyx] x' y' [Hxy' Hyx']. split. - apply wedge_ol. + apply ex_ol. apply vee_l_ol. apply ex_ol... + apply ex_ol. apply vee_r_ol. apply ex_ol... - apply wedge_ol. + apply ex_ol. apply vee_l_ol. apply ex_ol... + apply ex_ol. apply vee_r_ol. apply ex_ol... Qed. Lemma OL_wedge_com : forall x y, x ∧ y ≡ y ∧ x . Proof with try now apply I. intros x y. split. - apply ex_ol. apply wedge_ol. + apply ex_ol. apply vee_r_ol. apply ax_ol... + apply ex_ol. apply vee_l_ol. apply ax_ol... - apply ex_ol. apply wedge_ol. + apply ex_ol. apply vee_r_ol. apply ax_ol... + apply ex_ol. apply vee_l_ol. apply ax_ol... Qed. Lemma OL_wedge_assoc : forall x y z, x ∧ (y ∧ z) ≡ (x ∧ y) ∧ z . Proof with try now apply I. intros x y z. split. - apply ex_ol. apply wedge_ol. + apply wedge_ol ; apply ex_ol. * apply vee_l_ol. apply ax_ol... * apply vee_r_ol. apply vee_l_ol. apply ax_ol... + apply ex_ol. apply vee_r_ol. apply vee_r_ol. apply ax_ol... - apply ex_ol. apply wedge_ol. + apply ex_ol. apply vee_l_ol. apply vee_l_ol. apply ax_ol... + apply wedge_ol ; apply ex_ol. * apply vee_l_ol. apply vee_r_ol. apply ax_ol... * apply vee_r_ol. apply ax_ol... Qed. Lemma OL_wedge_idem : forall x, x ∧ x ≡ x . Proof with try now apply I. split. - apply vee_l_ol. apply ax_ol... - apply ex_ol. apply wedge_ol ; apply ex_ol ; apply ax_ol... Qed. Lemma OL_wedge_top : forall x, x ∧ ⊤ ≡ x . Proof with try now apply I. intros x. split. - apply vee_l_ol. apply ax_ol... - apply ex_ol. apply wedge_ol. + apply ex_ol. apply ax_ol... + apply top_ol. Qed. Lemma OL_top_wedge : forall x, ⊤ ∧ x ≡ x . Proof. intros x. rewrite OL_wedge_com. apply OL_wedge_top. Qed. Lemma OL_bot_wedge : forall x, ⊥ ∧ x ≡ ⊥ . Proof. intro x. split. - apply vee_l_ol. apply top_ol. - apply top_ol. Qed. Lemma OL_wedge_bot : forall x, x ∧ ⊥ ≡ ⊥ . Proof. intro x. rewrite OL_wedge_com. apply OL_bot_wedge. Qed. Lemma OL_contrad : forall x, x ∧ ¬ x ≡ ⊥ . Proof with try now apply I. intro x. split. - apply cw_ol... simpl. apply vee_r_ol. apply ex_ol. apply vee_l_ol. rewrite bidual. apply ax_ol... - apply top_ol. Qed. (** Second Focused System OLf **) Inductive seq_3 : Set := | fc | rv | rr . Inductive olf : seq_3 -> formula -> formula -> Prop := | ax_fc_olf : forall x, olf fc (covar x) (var x) | vee_l_fc_olf : forall C A B, olf fc C A -> olf fc C (vee A B) | vee_r_fc_olf : forall C A B, olf fc C A -> olf fc C (vee B A) | top_rv_olf : forall C, (sync C \/ is_covar C) -> olf rv C top | top_rr_olf : forall C, olf rr top C | wedge_rv_olf : forall C A B, olf rv C A -> olf rv C B -> olf rv C (wedge A B) | wedge_rr_olf : forall C A B, olf rr A C -> olf rr B C -> olf rr (wedge A B) C | unfoc_fc_olf : forall C A, async A -> olf rv C A -> olf fc C A | unrev_rr_olf : forall C A, olf rv A C -> olf rr A C | foc_l_rv_olf : forall A C, sync A -> olf fc C A -> olf rv A C | foc_r_rv_olf : forall A C, sync A -> olf fc C A -> olf rv C A | cw_rr_olf : forall A B C, olf fc (vee A B) (vee A B) -> olf rr (vee A B) C | cw_rv_olf : forall A B C, (sync C \/ is_covar C) -> olf fc (vee A B) (vee A B) -> olf rv C (vee A B) . Notation "⊦ A ⇓ B" := (olf fc A B) (at level 50). Notation "⊦ A ⇑ B" := (olf rv A B) (at level 50). Notation "⊦ ⇑ A , B" := (olf rr A B) (at level 50). (* Example 3.12 *) Example example_1_3_olf : forall x y, ⊦ ⇑ bot, vee (vee (wedge (var x) (var y)) (covar x)) (covar y) . Proof with try auto_sync_async. intros x y. apply unrev_rr_olf. apply cw_rv_olf... apply vee_l_fc_olf. apply vee_l_fc_olf. apply unfoc_fc_olf... apply wedge_rv_olf. - apply foc_l_rv_olf... apply vee_l_fc_olf. apply vee_r_fc_olf. apply unfoc_fc_olf... apply foc_l_rv_olf... apply ax_fc_olf. - apply foc_l_rv_olf... apply vee_r_fc_olf. apply unfoc_fc_olf... apply foc_l_rv_olf... apply ax_fc_olf. Qed. (* a version of olf with additional parameters and length *) Inductive polf {Pss : seq_3 -> formula -> formula -> Prop} {fs : nat -> nat -> nat} : seq_3 -> formula -> formula -> nat -> Prop := (* Pss can be used to constrain internal sequents with a predicate, fs is used for computing size in binary rules: typically plus or max last nat is proof "size" *) | ax_fc_polf : forall x, Pss fc (covar x) (var x) -> polf fc (covar x) (var x) 1 | vee_l_fc_polf : forall C A B l1, Pss fc C (vee A B) -> polf fc C A l1 -> polf fc C (vee A B) (S l1) | vee_r_fc_polf : forall C A B l1, Pss fc C (vee B A) -> polf fc C A l1 -> polf fc C (vee B A) (S l1) | top_rv_polf : forall C, Pss rv C top -> (sync C \/ is_covar C) -> polf rv C top 1 | top_rr_polf : forall C, Pss rr top C -> polf rr top C 1 | wedge_rv_polf : forall C A B l1 l2, Pss rv C (wedge A B) -> polf rv C A l1 -> polf rv C B l2 -> polf rv C (wedge A B) (S (fs l1 l2)) | wedge_rr_polf : forall C A B l1 l2, Pss rr (wedge A B) C -> polf rr A C l1 -> polf rr B C l2 -> polf rr (wedge A B) C (S (fs l1 l2)) | unfoc_fc_polf : forall C A l1, Pss fc C A -> async A -> polf rv C A l1 -> polf fc C A (S l1) | unrev_rr_polf : forall C A l1, Pss rr A C -> polf rv A C l1 -> polf rr A C (S l1) | foc_l_rv_polf : forall A C l1, Pss rv A C -> sync A -> polf fc C A l1 -> polf rv A C (S l1) | foc_r_rv_polf : forall A C l1, Pss rv C A -> sync A -> polf fc C A l1 -> polf rv C A (S l1) | cw_rr_polf : forall A B C l1, Pss rr (vee A B) C -> polf fc (vee A B) (vee A B) l1 -> polf rr (vee A B) C (S l1) | cw_rv_polf : forall A B C l1, Pss rv C (vee A B) -> (sync C \/ is_covar C) -> polf fc (vee A B) (vee A B) l1 -> polf rv C (vee A B) (S l1) . (* Pss is used to add structure on proofs, basic case is predicate True *) Notation "l ⊦ A ⇓ B" := (@polf (fun _ _ _ => True) max fc A B l) (at level 50). Notation "l ⊦ A ⇑ B" := (@polf (fun _ _ _ => True) max rv A B l) (at level 50). Notation "l ⊦ ⇑ A , B" := (@polf (fun _ _ _ => True) max rr A B l) (at level 50). Proposition olf_is_polf : forall fs t A B, olf t A B <-> exists l, (@polf (fun _ _ _ => True) fs t A B l) . Proof with try (now apply I) ; try eassumption ; try auto_sync_async. intros fs t A B. split. - intro pi. induction pi ; try (now eexists ; constructor ; try (now apply I)) ; try (now destruct IHpi as [l pi'] ; eexists ; constructor ; try (now apply I) ; try eassumption ; try auto_sync_async). + destruct IHpi as [l pi']. eexists. apply vee_r_fc_polf... + destruct IHpi1 as [l1 pi1']. destruct IHpi2 as [l2 pi2']. eexists. apply wedge_rv_polf... + destruct IHpi1 as [l1 pi1']. destruct IHpi2 as [l2 pi2']. eexists. apply wedge_rr_polf... + destruct IHpi as [l pi']. eexists. apply foc_r_rv_polf... + destruct IHpi as [l pi']. eexists. apply cw_rr_polf... + destruct IHpi as [l pi']. eexists. apply cw_rv_polf... - intros [l pi]. induction pi ; try (now constructor ; try eassumption ; try auto_sync_async). + apply vee_r_fc_olf... + apply foc_r_rv_olf... + apply cw_rr_olf... + apply cw_rv_olf... Qed. Lemma not_var_var_fc_polf : forall x y l, ~ l ⊦ var x ⇓ var y . Proof. intros x y l pi. inversion pi. inversion H0 ; inversion H1. Qed. Lemma not_bot_fc_polf : forall A l, ~ l ⊦ A ⇓ bot . Proof. intros A l pi. inversion pi. inversion H0 ; inversion H1. Qed. (* Proposition 3.13, Part 1 *) Proposition olf0_to_polf_0 : forall t A B l, olf0 t A B l -> (t = ll4 -> (exists l', l' ⊦ A ⇓ B /\ sync B) \/ (exists l', l' ⊦ B ⇓ A /\ sync A) \/ (exists l', l' ⊦ A ⇓ A /\ sync A) \/ (exists l', l' ⊦ B ⇓ B /\ sync B) ) /\ (t = fc4 -> (exists l', l' ⊦ A ⇓ B) \/ ((exists l', l' ⊦ A ⇓ A) /\ exists A1 A2, A = vee A1 A2)) /\ (t = rv4 -> (exists l', l' ⊦ A ⇑ B) \/ ((exists l', l' ⊦ A ⇓ A) /\ exists A1 A2, A = vee A1 A2)) /\ (t = rr4 -> exists l', l' ⊦ ⇑ A, B) . Proof with try reflexivity ; try eassumption ; try now auto_sync_async. intros t A B l pi. induction pi ; (split ; [ | split ; [ | split]]) ; intro Ht ; try (now inversion Ht) ; try (now eexists ; constructor ; assumption) ; try (now eexists ; constructor ; constructor) ; try (now left ; eexists ; constructor ; assumption) ; try (now left ; eexists ; constructor ; [ constructor | assumption ]) ; try (now left ; eexists ; constructor ; constructor ; assumption). - apply IHpi in Ht. destruct Ht as [[l' pi']|pi']. + left. eexists. apply vee_l_fc_polf... + right... - apply IHpi in Ht. destruct Ht as [[l' pi']|pi']. + left. eexists. apply vee_r_fc_polf... + right... - assert (Ht' := Ht). apply IHpi1 in Ht. apply IHpi2 in Ht'. destruct Ht as [[l' pi']|pi'] ; destruct Ht' as [[l'' pi'']|pi''] ; try (right ; assumption). left. eexists. apply wedge_rv_polf... - assert (Ht' := Ht). apply IHpi1 in Ht. apply IHpi2 in Ht'. destruct Ht as [l' pi']. destruct Ht' as [l'' pi'']. eexists. apply wedge_rr_polf... - assert (rv4 = rv4) as Ht'... apply IHpi in Ht'. destruct Ht' as [[l' pi']|pi']. + left. eexists. apply unfoc_fc_polf... + right... - assert (ll4 = ll4) as Ht'... apply IHpi in Ht'. destruct Ht' as [Hf|[Hf|[Hf|Hf]]] ; destruct Hf as [l' [Hf Hs]]. + left. eexists. apply foc_r_rv_polf... + left. eexists. apply foc_l_rv_polf... + inversion Hs ; subst. * apply not_var_var_fc_polf in Hf. destruct Hf. * apply not_bot_fc_polf in Hf. destruct Hf. * right. split ; eexists... eexists... + inversion Hs ; subst. * apply not_var_var_fc_polf in Hf. destruct Hf. * apply not_bot_fc_polf in Hf. destruct Hf. * apply ex_ll_olf0 in pi. apply left_is_sync_or_covar_ll_olf0 in pi. left. eexists. apply cw_rv_polf... - assert (rv4 = rv4) as Ht'... apply IHpi in Ht'. destruct Ht' as [[l' pi']|[[l' pi'] [A1 [A2 Hv]]]]. + eexists. apply unrev_rr_polf... + subst. eexists. apply cw_rr_polf... - assert (fc4 = fc4) as Ht'... apply IHpi in Ht'. destruct Ht' as [[l3 pi3]|[[l3 pi3] [A1 [A2 Hv]]]]. + right ; left. eexists. split... + right ; right ; right. subst. eexists. split... - assert (fc4 = fc4) as Ht'... apply IHpi in Ht'. destruct Ht' as [[l3 pi3]|[[l3 pi3] [A1 [A2 Hv]]]]. + left. eexists. split... + right ; right ; left. subst. eexists. split... - apply IHpi in Ht. right ; right ; left. inversion Ht as [Htt | [Htt | [Htt | Htt]]] ; destruct Htt as [ltt [Htt Hs]] ; eexists ; split... - apply IHpi in Ht. right ; right ; right. inversion Ht as [Htt | [Htt | [Htt | Htt]]] ; destruct Htt as [ltt [Htt Hs]] ; eexists ; split... Qed. (* Proposition 3.13, Part 2 *) Proposition olf0_to_polf : forall A B l, olf0 rr4 A B l -> exists l', l' ⊦ ⇑ A, B . Proof. intros A B l pi. apply olf0_to_polf_0 in pi. apply pi. reflexivity. Qed. (* Proposition 3.14 *) Proposition polf_to_ol : forall Pss fs t A B l, @polf Pss fs t A B l -> ⊦ A, B . Proof with try assumption ; try (apply ex_ol ; assumption) ; try now apply I. intros Pss fs t A B l pi. induction pi ; try (now constructor ; assumption) ; try (now apply ex_ol ; constructor ; assumption) ; try (now apply ex_ol ; constructor ; apply ex_ol ; assumption)... - apply ax_var_ol. - apply ex_ol. apply vee_r_ol... - apply cw_ol... - apply ex_ol. apply cw_ol... Qed. (* Soundness and Completeness of OLf wrt OL *) Theorem ol_iff_olf : forall A B, ⊦ A, B <-> ⊦ ⇑ A, B . Proof with assumption. intros A B. split ; intro pi. - apply atomic_ol in pi. apply vee_ol in pi. apply revert_ol in pi. apply ol_to_olf0 in pi. destruct pi as [l pi]. apply olf0_to_polf in pi. apply olf_is_polf in pi... - apply (olf_is_polf plus) in pi. destruct pi as [l pi]. apply polf_to_ol in pi... Qed. (* End of Section 3.4 *) Proposition cut_elim_olf : forall A B C, ⊦ ⇑ A, B -> ⊦ ⇑ dual B, C -> ⊦ ⇑ A, C . Proof. intros A B C pi1 pi2. apply ol_iff_olf. apply ol_iff_olf in pi1. apply ol_iff_olf in pi2. eapply cut_elim_ol ; eassumption. Qed. (** Backward Proof Search **) (* measure on formulas *) Fixpoint gsize A := match A with | var x => 1 | covar x => 1 | top => 1 | bot => 1 | wedge A B => gsize A + gsize B | vee A B => 2 * (gsize A + gsize B) end. Notation "'φ' A" := (gsize A) (at level 9). Lemma gsize_pos : forall A, 0 < gsize A . Proof. induction A ; simpl ; omega. Qed. Lemma gsize_small_0 : forall A, 2 * gsize A <= exp (fsize A) . Proof with try (simpl ; lia). induction A... - assert (He1 := exp_mon (fsize A1) (fsize A1 + fsize A2)). assert (He2 := exp_mon (fsize A2) (fsize A2 + fsize A1)). rewrite plus_comm in He2... - assert (He1 := exp_mon (fsize A1 + 1) (fsize A1 + fsize A2)). assert (He2 := exp_mon (1 + fsize A2) (fsize A1 + fsize A2)). assert (Hf1 := fsize_pos A1). assert (Hf2 := fsize_pos A2). assert (fsize A1 + 1 <= fsize A1 + fsize A2) as H1... apply He1 in H1. assert (1 + fsize A2 <= fsize A1 + fsize A2) as H2... apply He2 in H2. rewrite plus_comm in H1. simpl in H1. simpl in H2... Qed. Lemma gsize_small : forall A, gsize A < exp (fsize A) . Proof. intro A. assert (Hp := gsize_pos A). assert (Hs := gsize_small_0 A). omega. Qed. (* measure on sequents *) Fixpoint ssize t A B := match t with | fc => gsize A + gsize B + (match B with | var _ => 0 | covar _ => 1 + gsize B | bot => 0 | top => 1 + gsize B | vee _ _ => 0 | wedge _ _ => 1 + gsize B end) | rv => gsize A + 2 * gsize B | rr => 2 * (gsize A + gsize B) end. Notation "ψ(⊦ A ⇓ B )" := (ssize fc A B) (at level 40). Notation "ψ(⊦ A ⇑ B )" := (ssize rv A B) (at level 40). Notation "ψ(⊦ ⇑ A , B )" := (ssize rr A B) (at level 40). (* facts about ssize *) Fact f1 : forall A B C, ssize fc A B < ssize fc A (vee B C). Proof. intros. assert (Hs := gsize_pos C). case B ; intros ; simpl ; lia. Qed. Fact f2 : forall A B C, ssize fc A B < ssize fc A (vee C B). Proof. intros. assert (Hs := gsize_pos C). case B ; intros ; simpl ; lia. Qed. Fact f3 : forall t A B C, ssize t A B < ssize t A (wedge B C). Proof with try (simpl ; lia). intros. assert (Hs := gsize_pos C). case t... case B ; intros... Qed. Fact f4 : forall t A B C, ssize t A B < ssize t A (wedge C B). Proof with try (simpl ; lia). intros. assert (Hs := gsize_pos C). case t... case B ; intros... Qed. Fact f5 : forall A B, async B \/ is_covar B -> ssize rv A B < ssize fc A B. Proof. intros. destruct B ; try (now inversion H as [Ha | Ha] ; inversion Ha) ; simpl ; lia. Qed. Fact f6 : forall A B, ssize rv A B < ssize rr A B. Proof. intros. assert (He := gsize_pos A). simpl ; lia. Qed. Fact f7 : forall A B, sync B -> ssize fc A B < ssize rv A B. Proof with try (simpl ; lia). intros. destruct B ; try now inversion H... assert (Hs := gsize_pos B2)... Qed. Fact f8 : forall A B, sync B -> ssize fc A B < ssize rv B A. Proof. intros. assert (Hs := gsize_pos A). destruct B ; try now inversion H ; simpl ; lia. Qed. Fact f9 : forall A B, sync A -> ssize fc A A < ssize rr A B. Proof. intros. assert (Hs := gsize_pos B). destruct A ; try now inversion H ; simpl ; lia. Qed. Fact f10 : forall A B, sync A -> ssize fc A A < ssize rv B A. Proof. intros. assert (Hs := gsize_pos B). destruct A ; try now inversion H ; simpl ; lia. Qed. Fact f11 : forall A B C, ssize rr B A < ssize rr (wedge B C) A. Proof. intros. assert (Hs := gsize_pos C). simpl ; lia. Qed. Fact f12 : forall A B C, ssize rr B A < ssize rr (wedge C B) A. Proof. intros. assert (Hs := gsize_pos C). simpl ; lia. Qed. (* Proposition 4.1 *) Proposition exp_height_bound_polf : forall Pss t A B l, @polf Pss max t A B l -> l < ssize t A B . Proof with try auto_sync_async ; try lia. intros Pss t A B l pi. induction pi ; try (unfold ssize ; simpl ; omega). - assert (Hf := f1 C A B)... - assert (Hf := f2 C A B)... - assert (Hf1 := f3 rv C A B). assert (Hf2 := f4 rv C B A)... - assert (Hf1 := f11 C A B). assert (Hf2 := f12 C B A)... - assert (async A \/ is_covar A) as Ha... apply (f5 C A) in Ha... - assert (Hf := f6 A C)... - apply (f8 C A) in H0... - apply (f7 C A) in H0... - assert (sync (vee A B)) as Hs... apply (f9 (vee A B) C) in Hs... - assert (sync (vee A B)) as Hs... apply (f10 (vee A B) C) in Hs... Qed. (* sub-formula relation *) Inductive subform : formula -> formula -> Prop := | sub_id : forall A, subform A A | sub_vee_l : forall A B C, subform A B -> subform A (vee B C) | sub_vee_r : forall A B C, subform A B -> subform A (vee C B) | sub_wedge_l : forall A B C, subform A B -> subform A (wedge B C) | sub_wedge_r : forall A B C, subform A B -> subform A (wedge C B) . Lemma subform_size : forall A B, subform A B -> fsize A <= fsize B . Proof. intros A B Hs. induction Hs ; simpl ; omega. Qed. Lemma subform_trans : forall B C, subform B C -> forall A, subform A B -> subform A C . Proof with try assumption. intros B C Hs. induction Hs ; intros A0 Hs0 ; try apply IHHs in Hs0... - apply sub_vee_l... - apply sub_vee_r... - apply sub_wedge_l... - apply sub_wedge_r... Qed. (* sub-formula of R1 or R2 *) Definition bisubform A R1 R2 := subform A R1 \/ subform A R2 . (* Sub-Formula Property *) Proposition sub_formula_0 : forall fs R1 R2 t A B l, @polf (fun _ _ _ => True) fs t A B l -> bisubform A R1 R2 -> bisubform B R1 R2 -> @polf (fun t' A' B' => bisubform A' R1 R2 /\ bisubform B' R1 R2) fs t A B l . Proof with try eassumption ; try (now constructor) ; try (now split ; assumption). intros fs R1 R2 t A B l pi. induction pi ; intros Ps1 Ps2. - apply ax_fc_polf... - apply vee_l_fc_polf... apply IHpi... destruct Ps2 ; [left | right] ; eapply subform_trans ; try eassumption ; apply sub_vee_l... - apply vee_r_fc_polf... apply IHpi... destruct Ps2 ; [left | right] ; eapply subform_trans ; try eassumption ; apply sub_vee_r... - apply top_rv_polf... - apply top_rr_polf... - apply wedge_rv_polf... + apply IHpi1... destruct Ps2 ; [left | right] ; eapply subform_trans ; try eassumption ; apply sub_wedge_l... + apply IHpi2... destruct Ps2 ; [left | right] ; eapply subform_trans ; try eassumption ; apply sub_wedge_r... - apply wedge_rr_polf... + apply IHpi1... destruct Ps1 ; [left | right] ; eapply subform_trans ; try eassumption ; apply sub_wedge_l... + apply IHpi2... destruct Ps1 ; [left | right] ; eapply subform_trans ; try eassumption ; apply sub_wedge_r... - apply unfoc_fc_polf... apply IHpi... - apply unrev_rr_polf... apply IHpi... - apply foc_l_rv_polf... apply IHpi... - apply foc_r_rv_polf... apply IHpi... - apply cw_rr_polf... apply IHpi... - apply cw_rv_polf... apply IHpi... Qed. Proposition sub_formula : forall fs t A B l, @polf (fun _ _ _ => True) fs t A B l -> @polf (fun t' A' B' => bisubform A' A B /\ bisubform B' A B) fs t A B l . Proof with try now constructor. intros fs t A B l pi. apply sub_formula_0. - assumption. - left... - right... Qed. (* sub-formula relation with position inside formula tree *) Inductive subform_pos : formula -> formula -> nat -> Prop := | sub_pos_id : forall A, subform_pos A A 0 | sub_pos_vee_l : forall A B C i, subform_pos A B i -> subform_pos A (vee B C) (S i) | sub_pos_vee_r : forall A B C i, subform_pos A B i -> subform_pos A (vee C B) (fsize C + S i) | sub_pos_wedge_l : forall A B C i, subform_pos A B i -> subform_pos A (wedge B C) (S i) | sub_pos_wedge_r : forall A B C i, subform_pos A B i -> subform_pos A (wedge C B) (fsize C + S i) . Lemma subform_exists_pos : forall A B, subform A B <-> exists i, subform_pos A B i . Proof with try eassumption. intros A B. split ; intro Hs. - induction Hs ; try (now eexists ; constructor) ; destruct IHHs as [i Hsi] ; eexists. + apply sub_pos_vee_l... + apply sub_pos_vee_r... + apply sub_pos_wedge_l... + apply sub_pos_wedge_r... - destruct Hs as [i Hsi]. induction Hsi. + apply sub_id. + apply sub_vee_l... + apply sub_vee_r... + apply sub_wedge_l... + apply sub_wedge_r... Qed. Lemma subform_small : forall A B i, subform_pos A B i -> i < fsize B . Proof. intros A B i Hs. induction Hs ; simpl ; try omega. apply fsize_pos. Qed. Lemma subform_uniq_pos : forall A B C i, subform_pos A C i -> subform_pos B C i -> A = B . Proof with try assumption ; try reflexivity ; try omega. intros A B C i Hs. induction Hs ; intro Hs'. - inversion Hs'... - inversion Hs'... + apply IHHs... + apply subform_small in Hs... - inversion Hs'... + apply subform_small in H1... + apply IHHs... assert (i = i0)... subst... - inversion Hs'... + apply IHHs... + apply subform_small in Hs... - inversion Hs'... + apply subform_small in H1... + apply IHHs... assert (i = i0)... subst... Qed. (* sub-formula with position wrt a pair of formulas *) Definition bisubform_pos A R1 R2 i := subform_pos A R1 i \/ exists j, subform_pos A R2 j /\ i = j + fsize R1 . Lemma bisubform_exists_pos : forall A R1 R2, bisubform A R1 R2 <-> exists i, bisubform_pos A R1 R2 i . Proof with try eassumption ; try reflexivity. intros A R1 R2. split ; intro Hs. - destruct Hs as [Hs | Hs]. + apply subform_exists_pos in Hs. destruct Hs as [i Hsi]. eexists i. left... + apply subform_exists_pos in Hs. destruct Hs as [i Hsi]. exists (i + fsize R1). right. exists i. split... - destruct Hs as [i [Hsi | Hsi]] ; [left | right] ; apply subform_exists_pos. + eexists... + destruct Hsi as [j [Hsj Hsi]]. eexists... Qed. Lemma bisubform_small : forall A R1 R2 i, bisubform_pos A R1 R2 i -> i < fsize R1 + fsize R2 . Proof with try (simpl ; omega). intros A R1 R2 i Hs. destruct Hs as [Hs | Hs]. - apply subform_small in Hs... - destruct Hs as [j [Hj Hi]]. apply subform_small in Hj... Qed. Lemma bisubform_uniq_pos : forall A B R1 R2 i, bisubform_pos A R1 R2 i -> bisubform_pos B R1 R2 i -> A = B . Proof with try eassumption ; try reflexivity ; try omega. intros A B R1 R2 i Hs. induction Hs ; intro Hs' ; inversion Hs'. - eapply subform_uniq_pos... - destruct H0 as [j [Hj Hi]]. apply subform_small in H. apply subform_small in Hj... - destruct H as [j [Hj Hi]]. apply subform_small in H0. apply subform_small in Hj... - destruct H as [j1 [Hj1 Hi1]]. destruct H0 as [j2 [Hj2 Hi2]]. assert (j1 = j2)... subst. eapply subform_uniq_pos... Qed. (* existence of functions e1 e2 e3 which extract sequents along a branch *) Proposition bounding_functions : forall R1 R2 t A B l, @polf (fun t' A' B' => bisubform A' R1 R2 /\ bisubform B' R1 R2) max t A B l -> exists e1 e2 e3, forall n, (S n < l -> ssize (e1 n) (e2 n) (e3 n) < ssize (e1 (S n)) (e2 (S n)) (e3 (S n))) /\ (S n = l -> ssize (e1 n) (e2 n) (e3 n) = ssize t A B) /\ (n < l -> bisubform (e2 n) R1 R2 /\ bisubform (e3 n) R1 R2) . Proof with try eassumption ; try omega ; try auto_sync_async. intros R1 R2 t A B l pi. induction pi ; try destruct IHpi as [e1 [e2 [e3 He]]]. - exists (fun n => fc). exists (fun n => covar x). exists (fun n => var x). intro n. split ; [ | split] ; intro Hl... - exists (fun n => if (leb (S n) l1) then e1 n else fc). exists (fun n => if (leb (S n) l1) then e2 n else C). exists (fun n => if (leb (S n) l1) then e3 n else vee A B). intro n. split ; [ | split] ; intro Hl. + case_bool (S n) l1; rename HHeq into HHeq' ; case_bool (S (S n)) l1... * apply He... * assert (S n = l1)... subst. assert (ssize (e1 n) (e2 n) (e3 n) = ssize fc C A) as Hss by (apply He ; reflexivity). assert (Hf := f1 C A B)... + case_bool (S n) l1... + case_bool (S n) l1... apply He... - exists (fun n => if (leb (S n) l1) then e1 n else fc). exists (fun n => if (leb (S n) l1) then e2 n else C). exists (fun n => if (leb (S n) l1) then e3 n else vee B A). intro n. split ; [ | split] ; intro Hl. + case_bool (S n) l1; rename HHeq into HHeq' ; case_bool (S (S n)) l1... * apply He... * assert (S n = l1)... subst. assert (ssize (e1 n) (e2 n) (e3 n) = ssize fc C A) as Hss by (apply (He n) ; omega). assert (Hf := f2 C A B)... + case_bool (S n) l1... + case_bool (S n) l1... apply He... - exists (fun n => rv). exists (fun n => C). exists (fun n => top). intro n. split ; [ | split] ; intro Hl... - exists (fun n => rr). exists (fun n => top). exists (fun n => C). intro n. split ; [ | split] ; intro Hl... - destruct (Max.max_dec l1 l2) as [Hmax | Hmax] ; rewrite Hmax ; clear Hmax. { destruct IHpi1 as [e1 [e2 [e3 He]]]. exists (fun n => if (leb (S n) l1) then e1 n else rv). exists (fun n => if (leb (S n) l1) then e2 n else C). exists (fun n => if (leb (S n) l1) then e3 n else wedge A B). intro n. split ; [ | split] ; intro Hl. + case_bool (S n) l1; rename HHeq into HHeq' ; case_bool (S (S n)) l1... * apply He... * assert (S n = l1)... subst. assert (ssize (e1 n) (e2 n) (e3 n) = ssize rv C A) as Hss by (apply He ; reflexivity). assert (Hf := f3 rv C A B)... + case_bool (S n) l1... + case_bool (S n) l1... apply He... }{ destruct IHpi2 as [e1 [e2 [e3 He]]]. exists (fun n => if (leb (S n) l2) then e1 n else rv). exists (fun n => if (leb (S n) l2) then e2 n else C). exists (fun n => if (leb (S n) l2) then e3 n else wedge A B). intro n. split ; [ | split] ; intro Hl. + case_bool (S n) l2; rename HHeq into HHeq' ; case_bool (S (S n)) l2... * apply He... * assert (S n = l2)... subst. assert (ssize (e1 n) (e2 n) (e3 n) = ssize rv C B) as Hss by (apply He ; reflexivity). assert (Hf := f4 rv C B A)... + case_bool (S n) l2... + case_bool (S n) l2... apply He... } - destruct (Max.max_dec l1 l2) as [Hmax | Hmax] ; rewrite Hmax ; clear Hmax. { destruct IHpi1 as [e1 [e2 [e3 He]]]. exists (fun n => if (leb (S n) l1) then e1 n else rr). exists (fun n => if (leb (S n) l1) then e2 n else wedge A B). exists (fun n => if (leb (S n) l1) then e3 n else C). intro n. split ; [ | split] ; intro Hl. + case_bool (S n) l1; rename HHeq into HHeq' ; case_bool (S (S n)) l1... * apply He... * assert (S n = l1)... subst. assert (ssize (e1 n) (e2 n) (e3 n) = ssize rr A C) as Hss by (apply He ; reflexivity). assert (Hf := f11 C A B)... + case_bool (S n) l1... + case_bool (S n) l1... apply He... }{ destruct IHpi2 as [e1 [e2 [e3 He]]]. exists (fun n => if (leb (S n) l2) then e1 n else rr). exists (fun n => if (leb (S n) l2) then e2 n else wedge A B). exists (fun n => if (leb (S n) l2) then e3 n else C). intro n. split ; [ | split] ; intro Hl. + case_bool (S n) l2; rename HHeq into HHeq' ; case_bool (S (S n)) l2... * apply He... * assert (S n = l2)... subst. assert (ssize (e1 n) (e2 n) (e3 n) = ssize rr B C) as Hss by (apply He ; reflexivity). assert (Hf := f12 C B A)... + case_bool (S n) l2... + case_bool (S n) l2... apply He... } - exists (fun n => if (leb (S n) l1) then e1 n else fc). exists (fun n => if (leb (S n) l1) then e2 n else C). exists (fun n => if (leb (S n) l1) then e3 n else A). intro n. split ; [ | split] ; intro Hl. + case_bool (S n) l1; rename HHeq into HHeq' ; case_bool (S (S n)) l1... * apply He... * assert (S n = l1)... subst. assert (ssize (e1 n) (e2 n) (e3 n) = ssize rv C A) as Hss. apply He... rewrite Hss. assert (async A \/ is_covar A) as Ha... apply (f5 C A) in Ha... + case_bool (S n) l1... + case_bool (S n) l1... apply He... - exists (fun n => if (leb (S n) l1) then e1 n else rr). exists (fun n => if (leb (S n) l1) then e2 n else A). exists (fun n => if (leb (S n) l1) then e3 n else C). intro n. split ; [ | split] ; intro Hl. + case_bool (S n) l1; rename HHeq into HHeq' ; case_bool (S (S n)) l1... * apply He... * assert (S n = l1)... subst. assert (ssize (e1 n) (e2 n) (e3 n) = ssize rv A C) as Hss by (apply He ; reflexivity). assert (Hf := f6 A C)... + case_bool (S n) l1... + case_bool (S n) l1... apply He... - exists (fun n => if (leb (S n) l1) then e1 n else rv). exists (fun n => if (leb (S n) l1) then e2 n else A). exists (fun n => if (leb (S n) l1) then e3 n else C). intro n. split ; [ | split] ; intro Hl. + case_bool (S n) l1; rename HHeq into HHeq' ; case_bool (S (S n)) l1... * apply He... * assert (S n = l1)... subst. assert (ssize (e1 n) (e2 n) (e3 n) = ssize fc C A) as Hss by (apply He ; reflexivity). apply (f8 C A) in H0... + case_bool (S n) l1... + case_bool (S n) l1... apply He... - exists (fun n => if (leb (S n) l1) then e1 n else rv). exists (fun n => if (leb (S n) l1) then e2 n else C). exists (fun n => if (leb (S n) l1) then e3 n else A). intro n. split ; [ | split] ; intro Hl. + case_bool (S n) l1; rename HHeq into HHeq' ; case_bool (S (S n)) l1... * apply He... * assert (S n = l1)... subst. assert (ssize (e1 n) (e2 n) (e3 n) = ssize fc C A) as Hss by (apply He ; reflexivity). apply (f7 C A) in H0... + case_bool (S n) l1... + case_bool (S n) l1... apply He... - exists (fun n => if (leb (S n) l1) then e1 n else rr). exists (fun n => if (leb (S n) l1) then e2 n else vee A B). exists (fun n => if (leb (S n) l1) then e3 n else C). intro n. split ; [ | split] ; intro Hl. + case_bool (S n) l1; rename HHeq into HHeq' ; case_bool (S (S n)) l1... * apply He... * assert (S n = l1)... subst. assert (ssize (e1 n) (e2 n) (e3 n) = ssize fc (vee A B) (vee A B)) as Hss by (apply He ; reflexivity). assert (sync (vee A B)) as Hs... apply (f9 (vee A B) C) in Hs... + case_bool (S n) l1... + case_bool (S n) l1... apply He... - exists (fun n => if (leb (S n) l1) then e1 n else rv). exists (fun n => if (leb (S n) l1) then e2 n else C). exists (fun n => if (leb (S n) l1) then e3 n else vee A B). intro n. split ; [ | split] ; intro Hl. + case_bool (S n) l1; rename HHeq into HHeq' ; case_bool (S (S n)) l1... * apply He... * assert (S n = l1)... subst. assert (ssize (e1 n) (e2 n) (e3 n) = ssize fc (vee A B) (vee A B)) as Hss by (apply He ; reflexivity). assert (sync (vee A B)) as Hs... apply (f10 (vee A B) C) in Hs... + case_bool (S n) l1... + case_bool (S n) l1... apply He... Qed. Lemma bound_t : exists e : seq_3 -> nat, ((forall t, e t < 3) /\ (forall t1 t2, e t1 = e t2 -> t1 = t2)) . Proof. eexists (fun t => match t with fc => 0 | rv => 1 | rr => 2 end). split. - destruct t ; omega. - intros t1 t2. destruct t1 ; destruct t2 ; try reflexivity ; omega. Qed. (* position as a function *) Lemma bound_f : forall R1 R2 l, forall e0, (forall n, n < l -> bisubform (e0 n) R1 R2) -> exists e, ((forall n, n < l -> e n < fsize R1 + fsize R2) /\ (forall n m, n < l -> m < l -> e n = e m -> e0 n = e0 m)) . Proof with try eassumption ; try omega. intros R1 R2 l e0 He. assert (HH := (fchoice_finite l (fun x y => bisubform_pos (e0 x) R1 R2 y) (fun x Hl => (proj1 (bisubform_exists_pos (e0 x) R1 R2)) (He x Hl)))). destruct HH as [f HHf]. exists (fun n => if leb (S n) l then f n else 0). split. - intros n Hl. case_bool (S n) l. + specialize HHf with n. apply HHf in Hl. eapply bisubform_small... + assert (Hp := fsize_pos R1)... - intros n m Hn Hm. case_bool (S n) l ; rename HHeq into HHeq' ; case_bool (S m) l... intro Hmn. assert (HHn := HHf n Hn). assert (HHm := HHf m Hm). rewrite <- Hmn in HHm. eapply bisubform_uniq_pos... Qed. (* Polynomial Bound on Height of Proofs *) (* End of Section 4.1, Part 1 *) Proposition poly_height_bound_polf : forall A B l, l ⊦ ⇑ A, B -> l <= 3 * (fsize A + fsize B) * (fsize A + fsize B) . Proof with try assumption ; try omega. intros R1 R2 l pi. apply bound_inj_fun. apply sub_formula in pi. apply bounding_functions in pi. destruct pi as [e1 [e2 [e3 He]]]. assert (Hf := bound_t). assert (forall n, n < l -> bisubform (e2 n) R1 R2) as He2 by (intro ; apply He). assert (forall n, n < l -> bisubform (e3 n) R1 R2) as He3 by (intro ; apply He). apply bound_f in He2. apply bound_f in He3. destruct Hf as [f1 [Hf1b Hf1i]]. destruct He2 as [f2 [Hf2b Hf2i]]. destruct He3 as [f3 [Hf3b Hf3i]]. exists (fun k => if leb (S k) l then (f1 (e1 k) * ((fsize R1 + fsize R2) * (fsize R1 + fsize R2))) + (f2 k * (fsize R1 + fsize R2)) + f3 k else 0). split. - intros n Hl. case_bool (S n) l... specialize Hf1b with (e1 n). specialize Hf2b with n. specialize Hf3b with n. assert (Hl2 := Hl). apply Hf2b in Hl. apply Hf3b in Hl2. nia. - intros n m Hn Hm H. case_bool (S n) l ; rename HHeq into HHeq' ; case_bool (S m) l... assert (Hpos1 := fsize_pos R1). assert (Hpos2 := fsize_pos R2). specialize Hf1i with (e1 n) (e1 m). assert (Hf2i' := Hf2i n m Hn Hm). assert (Hf3i' := Hf3i n m Hn Hm). assert (Hf2bn := Hf2b n Hn). assert (Hf3bn := Hf3b n Hn). assert (Hf2bm := Hf2b m Hm). assert (Hf3bm := Hf3b m Hm). assert (f3 n = f3 m) as He3 by (apply (uniq_euclid_divid _ (f1 (e1 m) * (fsize R1 + fsize R2) + f2 m) (fsize R1 + fsize R2) (f1 (e1 n) * (fsize R1 + fsize R2) + f2 n)) ; nia). assert (f2 n = f2 m) as He2 by (apply (uniq_euclid_divid _ (f1 (e1 m)) (fsize R1 + fsize R2) (f1 (e1 n))) ; nia). assert (f1 (e1 n) = f1 (e1 m)) as He1 by (rewrite He2 in H ; rewrite He3 in H ; nia). apply Hf1i in He1. apply Hf2i' in He2. apply Hf3i' in He3. assert (forall n, (S n < l -> ssize (e1 n) (e2 n) (e3 n) < ssize (e1 (S n)) (e2 (S n)) (e3 (S n)))) as Hi by apply He. assert (Hi' := inc_fun (fun x => ssize (e1 x) (e2 x) (e3 x)) l Hi). simpl in Hi'. assert (Hi'' := injective_inc_fun _ _ Hi'). apply Hi''... rewrite He1. rewrite He2. rewrite He3... Qed. (* End of Section 4.1, Part 2 *) Proposition size_to_height_polf : forall Pss t A B s, @polf Pss plus t A B s -> exists h, @polf Pss max t A B h /\ s < exp h . Proof with try assumption ; try (simpl ; omega). intros Pss t A B s pi. induction pi ; try (exists 1 ; split ; [constructor ; assumption | simpl ; omega]) ; try (destruct IHpi as [h [pi' Ho]] ; exists (S h) ; split ; [constructor ; assumption | simpl ; omega]). - destruct IHpi as [h [pi' Ho]]... exists (S h). split... apply vee_r_fc_polf... - destruct IHpi1 as [h1 [pi1' Ho1]]... destruct IHpi2 as [h2 [pi2' Ho2]]... exists (S (max h1 h2)). split. + apply wedge_rv_polf... + simpl. assert (Hmax := mon_max _ h1 h2 exp_mon). nia. - destruct IHpi1 as [h1 [pi1' Ho1]]... destruct IHpi2 as [h2 [pi2' Ho2]]... exists (S (max h1 h2)). split. + apply wedge_rr_polf... + simpl. assert (Hmax := mon_max _ h1 h2 exp_mon). nia. - destruct IHpi as [h [pi' Ho]]... exists (S h). split... apply foc_r_rv_polf... - destruct IHpi as [h [pi' Ho]]... exists (S h). split... apply cw_rr_polf... - destruct IHpi as [h [pi' Ho]]... exists (S h). split... apply cw_rv_polf... Qed. Proposition exp_size_bound_polf : forall A B s, @polf (fun _ _ _ => True) plus rr A B s -> s < exp (3 * (fsize A + fsize B) * (fsize A + fsize B)) . Proof. intros A B s pi. apply size_to_height_polf in pi. destruct pi as [h [pi Hb]]. apply poly_height_bound_polf in pi. apply exp_mon in pi. omega. Qed. (** Single Formula Proof Search **) Inductive free_at : Atom -> formula -> Prop := | fvar : forall x, free_at x (var x) | fcovar : forall x, free_at x (covar x) | fwedgel : forall x A B, free_at x A -> free_at x (wedge A B) | fwedger : forall x A B, free_at x A -> free_at x (wedge B A) | fveel : forall x A B, free_at x A -> free_at x (vee A B) | fveer : forall x A B, free_at x A -> free_at x (vee B A) . Parameter eqat : Atom -> Atom -> bool. Parameter eqateq : forall x y, eqat x y = true <-> x = y. Parameter X : Atom. Parameter Y : Atom. Parameter two_at : X <> Y. Definition XX := ν X ∨ ν Y. Definition YY := ((ν X ∨ ν Y) ∧ κ X) ∨ ν X. Lemma leq_YY_XX : OL_leq YY XX. Proof with try now apply I. apply wedge_ol. - apply vee_l_ol. change XX with (dual (wedge (covar X) (covar Y))). apply ex_ol. apply ax_ol... - apply ex_ol. apply vee_l_ol. change (var X) with (dual (covar X)). apply ax_ol... Qed. Lemma inf_XX_YY : XX ∧ YY ≡ YY. Proof with try now apply I. split. - apply vee_r_ol. apply ax_ol... - apply ex_ol. apply wedge_ol ; apply ex_ol. + apply leq_YY_XX. + apply ax_ol... Qed. Lemma inf_XX_nYY : XX ∧ ¬YY ≡ ⊥. Proof with try now apply I. split. - apply cw_ol... apply vee_r_ol. apply vee_l_ol. apply wedge_ol ; apply ex_ol. + apply vee_l_ol. change (wedge (covar X) (covar Y)) with (dual (vee (var X) (var Y))). apply ax_ol... + apply vee_r_ol. apply vee_r_ol. change (var X) with (dual (covar X)). apply ax_ol... - apply top_ol. Qed. Lemma not_top_bot : ~ ⊤ ≡ ⊥. Proof. intros [H _]. apply ol_iff_olf in H. inversion H. inversion H0. - inversion H4. inversion H5. - inversion H4. inversion H5. Qed. Lemma not_leq_top_XX : ~ OL_leq (⊤) XX. Proof. intros H. apply ol_iff_olf in H. inversion H. inversion H0. - inversion H4. inversion H5. - inversion H4. + inversion H10. inversion H11. + inversion H10. inversion H11. + inversion H5. - inversion H7. + inversion H11. inversion H12. + inversion H11. inversion H12. + inversion H8. Qed. Lemma not_top_XX : ~ ⊤ ≡ XX. Proof. intros [H _]. apply not_leq_top_XX. assumption. Qed. Lemma not_leq_top_nYY : ~ OL_leq (⊤) (¬ YY). Proof. intros H. apply ol_iff_olf in H. inversion H. inversion H0. - inversion H7. + inversion H9. inversion H10. + inversion H9. inversion H13. * inversion H17. inversion H18. * inversion H14. - inversion H4. inversion H5. - inversion H1. Qed. Lemma not_top_nYY : ~ ⊤ ≡ ¬YY. Proof. intros [H _]. apply not_leq_top_nYY. assumption. Qed. Lemma not_leq_top_nXX : ~ OL_leq (⊤) (¬ XX). Proof. intros H. apply not_leq_top_nYY. transitivity (dual XX). - assumption. - apply OL_leq_dec. apply leq_YY_XX. Qed. Lemma not_top_nXX : ~ ⊤ ≡ ¬XX. Proof. intros [H _]. apply not_leq_top_nXX. assumption. Qed. Lemma not_leq_top_YY : ~ OL_leq (⊤) YY. Proof. intros H. apply not_leq_top_XX. transitivity YY. - assumption. - apply leq_YY_XX. Qed. Lemma not_top_YY : ~ ⊤ ≡ YY. Proof. intros [H _]. apply not_leq_top_YY. assumption. Qed. Lemma not_leq_nXX_XX : ~ OL_leq (¬XX) XX. Proof. intros H. apply ol_iff_olf in H. inversion H. - inversion H0. + inversion H4. * inversion H10. inversion H11. * inversion H10. inversion H11. * inversion H5. + inversion H4. * inversion H10. inversion H11. * inversion H10. inversion H11. * inversion H5. + inversion H7. * inversion H11. inversion H12. * inversion H11. inversion H12. * inversion H8. - inversion H2. + inversion H7. inversion H8. + inversion H7. inversion H8. + inversion H4. Qed. Lemma not_XX_nXX : ~ XX ≡ ¬XX. Proof. intros [_ H]. apply not_leq_nXX_XX. assumption. Qed. Lemma unprov_YY_YY : ~ ⊦ YY ⇓ YY. Proof with try assumption. intros H. inversion H. - inversion H3. inversion H5. + inversion H10. * inversion H14. inversion H20. inversion H22. inversion H27. apply not_leq_nXX_XX. apply ol_iff_olf. rewrite bidual. apply cw_rr_olf... apply not_leq_nXX_XX. apply ol_iff_olf. rewrite bidual. apply cw_rr_olf... apply not_leq_nXX_XX. apply ol_iff_olf. rewrite bidual. apply cw_rr_olf... inversion H26. inversion H32. inversion H33. inversion H32. inversion H33. inversion H27. inversion H23. inversion H20. inversion H21. inversion H15. * inversion H14. inversion H20. inversion H21. inversion H20. inversion H21. inversion H15. * apply not_leq_nXX_XX. apply ol_iff_olf. rewrite bidual. apply cw_rr_olf... + inversion H9. * inversion H15. inversion H17. inversion H24. inversion H25. inversion H25. inversion H18. inversion H18. * inversion H15. inversion H16. * inversion H10. + inversion H6. - inversion H3. inversion H4. - inversion H0. Qed. Lemma unprov_nXX_YY : ~ ⊦ ⇑ ¬XX, YY. Proof. intros H. inversion H. - inversion H3. inversion H5. + inversion H6. + inversion H9. * inversion H15. inversion H17. inversion H24. inversion H25. inversion H25. inversion H18. inversion H18. * inversion H15. apply two_at. rewrite H17. reflexivity. inversion H16. * inversion H10. + apply unprov_YY_YY. assumption. - inversion H0. + inversion H1. + inversion H4. * inversion H10. inversion H12. inversion H19. inversion H20. inversion H20. inversion H13. inversion H13. * inversion H10. inversion H11. * inversion H5. + inversion H5 ; inversion H8. Qed. Lemma not_leq_nYY_YY : ~ OL_leq (¬YY) YY. Proof with try assumption. intros H. apply ol_iff_olf in H. inversion H. - inversion H0 ; apply unprov_YY_YY... - apply unprov_YY_YY... Qed. Lemma not_YY_nYY : ~ YY ≡ ¬YY. Proof. intros [_ H]. apply not_leq_nYY_YY. assumption. Qed. Lemma not_leq_nYY_XX : ~ OL_leq (¬YY) XX. Proof with assumption. intro H. apply ol_iff_olf in H. inversion H. - inversion H0. + inversion H4. * inversion H10. inversion H12. inversion H17. apply not_leq_nXX_XX. apply ol_iff_olf. rewrite bidual. apply cw_rr_olf... apply not_leq_nXX_XX. apply ol_iff_olf. rewrite bidual. apply cw_rr_olf... apply not_leq_nXX_XX. apply ol_iff_olf. rewrite bidual. apply cw_rr_olf... inversion H16. inversion H22. inversion H23. inversion H22. inversion H23. inversion H17. inversion H13. * inversion H10. inversion H11. * inversion H5. + inversion H4. * inversion H10. inversion H11. * inversion H10. inversion H11. * inversion H5. + apply not_leq_nXX_XX. apply ol_iff_olf. rewrite bidual. apply cw_rr_olf... - apply unprov_YY_YY... Qed. Lemma not_XX_nYY : ~ XX ≡ ¬YY. Proof. intros [_ H]. apply not_leq_nYY_XX. assumption. Qed. Definition hex A := {A ≡ ⊤} + {A ≡ ⊥} + {A ≡ XX} + {A ≡ ¬ XX} + {A ≡ YY} + {A ≡ ¬ YY} . Lemma hex_dual : forall a, hex a -> hex (¬ a) . Proof with try reflexivity. intros a Ha. destruct Ha as [[[[[Ha | Ha] | Ha] | Ha] | Ha] | Ha]. - left ; left ; left ; left ; right. rewrite Ha ; simpl... - left ; left ; left ; left ; left. rewrite Ha ; simpl... - left ; left ; right. rewrite Ha ; simpl... - left ; left ; left ; right. rewrite Ha ; simpl... - right. rewrite Ha ; simpl... - left ; right. rewrite Ha ; simpl... Qed. Fact rwedge a b : hex a -> hex b -> formula. Proof. intros Ha Hb. destruct Ha as [[[[[Ha | Ha] | Ha] | Ha] | Ha] | Ha] ; destruct Hb as [[[[[Hb | Hb] | Hb] | Hb] | Hb] | Hb]. - apply top. - apply bot. - apply XX. - apply (dual XX). - apply YY. - apply (dual YY). - apply bot. - apply bot. - apply bot. - apply bot. - apply bot. - apply bot. - apply XX. - apply bot. - apply XX. - apply bot. - apply YY. - apply bot. - apply (dual XX). - apply bot. - apply bot. - apply (dual XX). - apply bot. - apply (dual XX). - apply YY. - apply bot. - apply YY. - apply bot. - apply YY. - apply bot. - apply (dual YY). - apply bot. - apply bot. - apply (dual XX). - apply bot. - apply (dual YY). Defined. Lemma hex_rwedge : forall a b Ha Hb, hex (rwedge a b Ha Hb) . Proof. intros a b Ha Hb. destruct Ha as [[[[[Ha | Ha] | Ha] | Ha] | Ha] | Ha] ; destruct Hb as [[[[[Hb | Hb] | Hb] | Hb] | Hb] | Hb] ; simpl ; try (rewrite Ha) ; try (rewrite Hb) ; try (left ; left ; left ; left ; left ; reflexivity) ; try (left ; left ; left ; left ; right ; reflexivity) ; try (left ; left ; left ; right ; reflexivity) ; try (left ; left ; right ; reflexivity) ; try (left ; right ; reflexivity) ; try (right ; reflexivity). Qed. Lemma rwedge_is_wedge : forall a b Ha Hb, rwedge a b Ha Hb ≡ wedge a b . Proof with try now constructor. intros a b Ha Hb. destruct Ha as [[[[[Ha | Ha] | Ha] | Ha] | Ha] | Ha] ; destruct Hb as [[[[[Hb | Hb] | Hb] | Hb] | Hb] | Hb] ; simpl ; rewrite Ha ; rewrite Hb ; try (rewrite OL_top_wedge) ; try (rewrite OL_wedge_top) ; try (rewrite OL_bot_wedge) ; try (rewrite OL_wedge_bot) ; try (rewrite OL_contrad) ; try (rewrite OL_wedge_idem) ; try (rewrite inf_XX_YY) ; try (rewrite OL_wedge_com ; rewrite inf_XX_YY) ; try (rewrite inf_XX_nYY) ; try (rewrite OL_wedge_com ; rewrite inf_XX_nYY) ; try (rewrite OL_wedge_com ; reflexivity) ; try reflexivity. - split. + apply top_ol. + apply cw_ol... apply vee_l_ol. apply ex_ol. apply vee_r_ol. apply leq_YY_XX. - split. + apply ex_ol. apply wedge_ol. * apply ax_ol... * apply wedge_ol. apply vee_l_ol. rewrite <- bidual at 1. apply ax_ol... apply ex_ol. apply vee_l_ol. rewrite <- bidual at 1. apply ax_ol... + apply vee_l_ol. apply ax_ol... - split. + apply top_ol. + apply cw_ol... apply vee_r_ol. apply ex_ol. apply vee_l_ol. apply leq_YY_XX. - split. + apply ex_ol. apply wedge_ol. * apply leq_YY_XX. * apply ax_ol... + apply vee_r_ol. apply ax_ol... Qed. Lemma dual_rwedge_dual_is_vee : forall a b Ha Hb, dual (rwedge (dual a) (dual b) (hex_dual a Ha) (hex_dual b Hb)) ≡ vee a b . Proof. intros a b Ha Hb. rewrite rwedge_is_wedge. simpl. rewrite_all bidual. reflexivity. Qed. Fact hex_top : hex top. Proof. left ; left ; left ; left ; left ; reflexivity. Defined. Fact hex_bot : hex bot. Proof. left ; left ; left ; left ; right ; reflexivity. Defined. Fact hex_XX : hex XX. Proof. left ; left ; left ; right ; reflexivity. Defined. Fact hex_nXX : hex (dual XX). Proof. left ; left ; right ; reflexivity. Defined. Fact hex_YY : hex YY. Proof. left ; right ; reflexivity. Defined. Fact hex_nYY : hex (dual YY). Proof. right ; reflexivity. Defined. Lemma hex_wedge : forall a b, hex a -> hex b -> hex (a ∧ b) . Proof with try reflexivity ; try (now constructor) ; try assumption. intros a b Ha Hb. destruct Ha as [[[[[Ha | Ha] | Ha] | Ha] | Ha] | Ha]. - destruct Hb as [[[[[Hb | Hb] | Hb] | Hb] | Hb] | Hb]. + left ; left ; left ; left ; left. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge top top hex_top hex_top)... + left ; left ; left ; left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge top bot hex_top hex_bot)... + left ; left ; left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge top XX hex_top hex_XX)... + left ; left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge top (dual XX) hex_top hex_nXX)... + left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge top YY hex_top hex_YY)... + right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge top (dual YY) hex_top hex_nYY)... - left ; left ; left ; left ; right. rewrite Ha. rewrite <- (rwedge_is_wedge bot b hex_bot Hb). destruct Hb as [[[[[Hb | Hb] | Hb] | Hb] | Hb] | Hb] ; simpl... - destruct Hb as [[[[[Hb | Hb] | Hb] | Hb] | Hb] | Hb]. + left ; left ; left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge XX top hex_XX hex_top)... + left ; left ; left ; left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge XX bot hex_XX hex_bot)... + left ; left ; left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge XX XX hex_XX hex_XX)... + left ; left ; left ; left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge XX (dual XX) hex_XX hex_nXX)... + left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge XX YY hex_XX hex_YY)... + left ; left ; left ; left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge XX (dual YY) hex_XX hex_nYY)... - destruct Hb as [[[[[Hb | Hb] | Hb] | Hb] | Hb] | Hb]. + left ; left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge (dual XX) top hex_nXX hex_top)... + left ; left ; left ; left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge (dual XX) bot hex_nXX hex_bot)... + left ; left ; left ; left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge (dual XX) XX hex_nXX hex_XX)... + left ; left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge (dual XX) (dual XX) hex_nXX hex_nXX)... + left ; left ; left ; left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge (dual XX) YY hex_nXX hex_YY)... + left ; left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge (dual XX) (dual YY) hex_nXX hex_nYY)... - destruct Hb as [[[[[Hb | Hb] | Hb] | Hb] | Hb] | Hb]. + left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge YY top hex_YY hex_top)... + left ; left ; left ; left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge YY bot hex_YY hex_bot)... + left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge YY XX hex_YY hex_XX)... + left ; left ; left ; left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge YY (dual XX) hex_YY hex_nXX)... + left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge YY YY hex_YY hex_YY)... + left ; left ; left ; left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge YY (dual YY) hex_YY hex_nYY)... - destruct Hb as [[[[[Hb | Hb] | Hb] | Hb] | Hb] | Hb]. + right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge (dual YY) top hex_nYY hex_top)... + left ; left ; left ; left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge (dual YY) bot hex_nYY hex_bot)... + left ; left ; left ; left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge (dual YY) XX hex_nYY hex_XX)... + left ; left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge (dual YY) (dual XX) hex_nYY hex_nXX)... + left ; left ; left ; left ; right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge (dual YY) YY hex_nYY hex_YY)... + right. rewrite Ha ; rewrite Hb. rewrite <- (rwedge_is_wedge (dual YY) (dual YY) hex_nYY hex_nYY)... Qed. Lemma hex_vee : forall a b, hex a -> hex b -> hex (a ∨ b) . Proof with assumption. intros a b Ha Hb. apply hex_dual in Ha. apply hex_dual in Hb. rewrite <- bidual. apply hex_dual. apply hex_wedge... Qed. Fixpoint subst A B x y C := match C with | var z => if eqat x z then A else if eqat y z then B else var z | covar z => if eqat x z then dual A else if eqat y z then dual B else covar z | wedge D E => wedge (subst A B x y D) (subst A B x y E) | vee D E => vee (subst A B x y D) (subst A B x y E) | bot => bot | top => top end. Definition bicontext h1 h2 f := forall h, free_at h f -> {h = h1} + {h = h2} . Lemma hex_subst : forall h1 h2 f, h1 <> h2 -> bicontext h1 h2 f -> forall a b, hex a -> hex b -> hex (subst a b h1 h2 f) . Proof with try reflexivity ; try assumption. intros h1 h2 f Hhh Hf. induction f ; intros A B HA HB. - assert (free_at a (ν a)) as Ha ; try (now constructor ; apply I). apply Hf in Ha. destruct Ha ; subst. + assert (eqat h1 h1 = true) as Heq by (rewrite eqateq ; reflexivity). simpl. rewrite Heq... + assert (eqat h1 h2 = false) as Heq1. * case_eq (eqat h1 h2) ; intro Heqat... rewrite eqateq in Heqat. apply Hhh in Heqat. inversion Heqat. * assert (eqat h2 h2 = true) as Heq by (rewrite eqateq ; reflexivity). simpl. rewrite Heq1. rewrite Heq... - assert (free_at a (κ a)) as Ha ; try (now constructor ; apply I). apply Hf in Ha. destruct Ha ; subst. + assert (eqat h1 h1 = true) as Heq by (rewrite eqateq ; reflexivity). simpl. rewrite Heq... apply hex_dual... + assert (eqat h1 h2 = false) as Heq1. * case_eq (eqat h1 h2) ; intro Heqat... rewrite eqateq in Heqat. apply Hhh in Heqat. inversion Heqat. * assert (eqat h2 h2 = true) as Heq by (rewrite eqateq ; reflexivity). simpl. rewrite Heq1. rewrite Heq... apply hex_dual... - apply hex_top. - apply hex_bot. - apply hex_wedge. + apply IHf1... intros h Hh. apply Hf. apply fwedgel... + apply IHf2... intros h Hh. apply Hf. apply fwedger... - apply hex_vee. + apply IHf1... intros h Hh. apply Hf. apply fveel... + apply IHf2... intros h Hh. apply Hf. apply fveer... Qed. Inductive values : Set := | Max | Min | Left | Right . Fixpoint vneg v := match v with | Max => Min | Min => Max | Left => Right | Right => Left end. Fact value : forall a, hex a -> values. Proof. intros a Ha. destruct Ha as [[[[[Ha | Ha] | Ha] | Ha] | Ha] | Ha]. - apply Max. - apply Min. - apply Left. - apply Right. - apply Left. - apply Right. Defined. Lemma value_inj : forall a b Ha Hb, a ≡ b -> value a Ha = value b Hb . Proof with try reflexivity ; try assumption. intros a b Ha Hb Heq. subst. destruct Ha as [[[[[Ha | Ha] | Ha] | Ha] | Ha] | Ha] ; destruct Hb as [[[[[Hb | Hb] | Hb] | Hb] | Hb] | Hb] ; simpl ; try reflexivity ; rewrite Ha in Heq ; rewrite Hb in Heq ; exfalso. - apply not_top_bot... - apply not_top_XX... - apply not_top_nXX... - apply not_top_YY... - apply not_top_nYY... - apply not_top_bot. rewrite Heq... - destruct Heq. apply ex_ol in H0. apply not_leq_top_nXX... - destruct Heq. apply ex_ol in H0. apply not_leq_top_XX... - destruct Heq. apply ex_ol in H0. apply not_leq_top_nYY... - destruct Heq. apply ex_ol in H0. apply not_leq_top_YY... - apply OL_equiv_sym in Heq. apply not_top_XX... - destruct Heq. apply ex_ol in H. apply not_leq_top_nXX... - apply not_XX_nXX... - destruct Heq. apply OL_leq_dec in H0. apply not_leq_nXX_XX. transitivity YY... apply leq_YY_XX. - apply OL_equiv_sym in Heq. apply not_top_nXX... - apply OL_equiv_sym in Heq. destruct Heq. apply ex_ol in H0. apply not_leq_top_XX... - apply OL_equiv_sym in Heq. apply not_XX_nXX... - destruct Heq. apply OL_leq_dec in H0. apply not_leq_nXX_XX. transitivity YY... apply leq_YY_XX. - apply OL_equiv_sym in Heq. apply not_top_YY... - destruct Heq. apply OL_leq_dec in H. apply not_leq_top_nYY... - destruct Heq. apply OL_leq_dec in H0. apply not_leq_nYY_XX... - destruct Heq. apply not_leq_nYY_YY... - apply OL_equiv_sym in Heq. apply not_top_nYY... - destruct Heq. apply OL_leq_dec in H. apply not_leq_top_YY... - destruct Heq. apply not_leq_nYY_XX... - destruct Heq. apply not_leq_nYY_YY... Qed. Lemma value_dual : forall a Ha Hna, value (dual a) Hna = vneg (value a Ha) . Proof with try reflexivity. intros a Ha Hna. assert (Ha' := Ha). destruct Ha as [[[[[Ha | Ha] | Ha] | Ha] | Ha] | Ha] ; destruct Hna as [[[[[Hna | Hna] | Hna] | Hna] | Hna] | Hna] ; try reflexivity ; exfalso ; rewrite Ha in Hna ; assert (Hs := OL_equiv_sym _ _ Hna) ; assert (Hd := OL_dual_compat _ _ Hna) ; assert (Hds := OL_equiv_sym _ _ Hd) ; try (apply not_top_bot ; assumption) ; try (apply not_top_XX ; assumption) ; try (apply not_top_nXX ; assumption) ; try (apply not_top_YY ; assumption) ; try (apply not_top_nYY ; assumption) ; try (apply not_XX_nXX ; assumption) ; try (apply not_XX_nYY ; assumption) ; try (apply not_YY_nYY ; assumption). Qed. Lemma rwedge_preciseness : forall a b c d Ha Hb Hc Hd, value a Ha = value c Hc -> value b Hb = value d Hd -> value (rwedge a b Ha Hb) (hex_rwedge a b Ha Hb) = value (rwedge c d Hc Hd) (hex_rwedge c d Hc Hd) . Proof with try reflexivity. intros a b c d Ha Hb Hc Hd Hv1 Hv2. assert (Ha' := Ha). assert (Hb' := Hb). assert (Hc' := Hc). assert (Hd' := Hd). destruct Ha as [[[[[Ha | Ha] | Ha] | Ha] | Ha] | Ha] ; destruct Hc as [[[[[Hc | Hc] | Hc] | Hc] | Hc] | Hc] ; simpl ; simpl in Hv1 ; inversion Hv1 ; destruct Hb as [[[[[Hb | Hb] | Hb] | Hb] | Hb] | Hb] ; destruct Hd as [[[[[Hd | Hd] | Hd] | Hd] | Hd] | Hd] ; simpl ; simpl in Hv2 ; inversion Hv2 ; try (rewrite (value_inj top top _ hex_top (OL_equiv_refl top)) ; simpl) ; try (rewrite (value_inj bot bot _ hex_bot (OL_equiv_refl bot)) ; simpl) ; try (rewrite (value_inj XX XX _ hex_XX (OL_equiv_refl XX)) ; simpl) ; try (rewrite (value_inj (dual XX) (dual XX) _ hex_nXX (OL_equiv_refl (dual XX))) ; simpl) ; try (rewrite (value_inj YY YY _ hex_YY (OL_equiv_refl YY)) ; simpl) ; try (rewrite (value_inj (dual YY) (dual YY) _ hex_nYY (OL_equiv_refl (dual YY))) ; simpl) ; try (rewrite (value_inj top top _ hex_top (OL_equiv_refl top)) ; simpl) ; try (rewrite (value_inj bot bot _ hex_bot (OL_equiv_refl bot)) ; simpl) ; try (rewrite (value_inj XX XX _ hex_XX (OL_equiv_refl XX)) ; simpl) ; try (rewrite (value_inj (dual XX) (dual XX) _ hex_nXX (OL_equiv_refl (dual XX))) ; simpl) ; try (rewrite (value_inj YY YY _ hex_YY (OL_equiv_refl YY)) ; simpl) ; try (rewrite (value_inj (dual YY) (dual YY) _ hex_nYY (OL_equiv_refl (dual YY))) ; simpl)... Qed. Lemma rcontext_preciseness : forall h1 h2 f (Hhh : h1 <> h2) (Hf : bicontext h1 h2 f), let syy := subst (¬XX) YY h1 h2 f in let sxx := subst (¬XX) XX h1 h2 f in value syy (hex_subst h1 h2 f Hhh Hf (dual XX) YY hex_nXX hex_YY) = value sxx (hex_subst h1 h2 f Hhh Hf (dual XX) XX hex_nXX hex_XX). Proof with try reflexivity ; try (now constructor) ; try assumption. intros h1 h2 f Hhh Hf syy sxx. unfold sxx. unfold syy. assert (HexXX := hex_XX). assert (HexYY := hex_YY). induction f. - assert (free_at a (ν a)) as Ha ; try (now constructor ; apply I). apply Hf in Ha. destruct Ha ; subst. + assert (eqat h1 h1 = true) as Heq by (rewrite eqateq ; reflexivity). assert (sxx ≡ (dual XX)) as Hxx by (unfold sxx ; simpl ; rewrite Heq ; reflexivity). assert (syy ≡ (dual XX)) as Hyy by (unfold syy ; simpl ; rewrite Heq ; reflexivity). unfold sxx in Hxx. subst. rewrite (value_inj sxx (dual XX) _ hex_nXX Hxx). unfold syy in Hyy. rewrite (value_inj syy (dual XX) _ hex_nXX Hyy)... + assert (eqat h1 h2 = false) as Heq1. { case_eq (eqat h1 h2) ; intro Heqat... rewrite eqateq in Heqat. apply Hhh in Heqat. inversion Heqat. } assert (eqat h2 h2 = true) as Heq by (rewrite eqateq ; reflexivity). assert (sxx ≡ XX) as Hxx by (unfold sxx ; simpl ; rewrite Heq1 ; rewrite Heq ; reflexivity). assert (syy ≡ YY) as Hyy by (unfold syy ; simpl ; rewrite Heq1 ; rewrite Heq ; reflexivity). unfold sxx in Hxx. rewrite (value_inj sxx XX _ hex_XX Hxx). unfold syy in Hyy. rewrite (value_inj syy YY _ hex_YY Hyy)... - assert (free_at a (κ a)) as Ha ; try (now constructor ; apply I). apply Hf in Ha. destruct Ha ; subst. + assert (eqat h1 h1 = true) as Heq by (rewrite eqateq ; reflexivity). assert (sxx ≡ XX) as Hxx by (unfold sxx ; simpl ; rewrite Heq ; reflexivity). assert (syy ≡ XX) as Hyy by (unfold syy ; simpl ; rewrite Heq ; reflexivity). unfold sxx in Hxx. rewrite (value_inj sxx XX _ hex_XX Hxx). unfold syy in Hyy. rewrite (value_inj syy XX _ hex_XX Hyy)... + assert (eqat h1 h2 = false) as Heq1. { case_eq (eqat h1 h2) ; intro Heqat... rewrite eqateq in Heqat. apply Hhh in Heqat. inversion Heqat. } assert (eqat h2 h2 = true) as Heq by (rewrite eqateq ; reflexivity). assert (sxx ≡ (dual XX)) as Hxx by (unfold sxx ; simpl ; rewrite Heq1 ; rewrite Heq ; reflexivity). assert (syy ≡ (dual YY)) as Hyy by (unfold syy ; simpl ; rewrite Heq1 ; rewrite Heq ; reflexivity). unfold sxx in Hxx. rewrite (value_inj sxx (dual XX) _ hex_nXX Hxx). unfold syy in Hyy. rewrite (value_inj syy (dual YY) _ hex_nYY Hyy)... - simpl. rewrite (value_inj top top _ hex_top (OL_equiv_refl top)). remember (value top hex_top) as Htop. rewrite (value_inj top top _ hex_top (OL_equiv_refl top))... - simpl. rewrite (value_inj bot bot _ hex_bot (OL_equiv_refl bot)). remember (value bot hex_bot) as Hbot. rewrite (value_inj bot bot _ hex_bot (OL_equiv_refl bot))... - assert (bicontext h1 h2 f13) as Hf1 by (intros h Hh ; apply Hf ; apply fwedgel ; assumption). assert (bicontext h1 h2 f14) as Hf2 by (intros h Hh ; apply Hf ; apply fwedger ; assumption). assert (hex (subst (¬XX) YY h1 h2 f13)) as Hex11 by (apply hex_subst ; try assumption ; apply hex_nXX). assert (hex (subst (¬XX) YY h1 h2 f14)) as Hex12 by (apply hex_subst ; try assumption ; apply hex_nXX). assert (hex (subst (¬XX) XX h1 h2 f13)) as Hex21 by (apply hex_subst ; try assumption ; apply hex_nXX). assert (hex (subst (¬XX) XX h1 h2 f14)) as Hex22 by (apply hex_subst ; try assumption ; apply hex_nXX). rewrite (value_inj (subst (¬XX) YY h1 h2 (f13 ∧ f14)) (rwedge (subst (¬XX) YY h1 h2 f13) (subst (¬XX) YY h1 h2 f14) Hex11 Hex12) _ (hex_rwedge (subst (¬XX) YY h1 h2 f13) (subst (¬XX) YY h1 h2 f14) Hex11 Hex12)). rewrite (value_inj (subst (¬XX) XX h1 h2 (f13 ∧ f14)) (rwedge (subst (¬XX) XX h1 h2 f13) (subst (¬XX) XX h1 h2 f14) Hex21 Hex22) _ (hex_rwedge (subst (¬XX) XX h1 h2 f13) (subst (¬XX) XX h1 h2 f14) Hex21 Hex22)). { apply rwedge_preciseness. - rewrite (value_inj (subst (¬XX) YY h1 h2 f13) (subst (¬XX) YY h1 h2 f13) Hex11 (hex_subst h1 h2 f13 Hhh Hf1 (¬XX) YY hex_nXX hex_YY) (OL_equiv_refl _)). rewrite (value_inj (subst (¬XX) XX h1 h2 f13) (subst (¬XX) XX h1 h2 f13) Hex21 (hex_subst h1 h2 f13 Hhh Hf1 (¬XX) XX hex_nXX hex_XX) (OL_equiv_refl _)). apply IHf1. - rewrite (value_inj (subst (¬XX) YY h1 h2 f14) (subst (¬XX) YY h1 h2 f14) Hex12 (hex_subst h1 h2 f14 Hhh Hf2 (¬XX) YY hex_nXX hex_YY) (OL_equiv_refl _)). rewrite (value_inj (subst (¬XX) XX h1 h2 f14) (subst (¬XX) XX h1 h2 f14) Hex22 (hex_subst h1 h2 f14 Hhh Hf2 (¬XX) XX hex_nXX hex_XX) (OL_equiv_refl _)). apply IHf2. } rewrite rwedge_is_wedge... rewrite rwedge_is_wedge... - assert (bicontext h1 h2 f13) as Hf1 by (intros h Hh ; apply Hf ; apply fveel ; assumption). assert (bicontext h1 h2 f14) as Hf2 by (intros h Hh ; apply Hf ; apply fveer ; assumption). assert (hex (subst (¬XX) YY h1 h2 f13)) as Hex11 by (apply hex_subst ; try assumption ; apply hex_nXX). assert (hex (subst (¬XX) YY h1 h2 f14)) as Hex12 by (apply hex_subst ; try assumption ; apply hex_nXX). assert (hex (subst (¬XX) XX h1 h2 f13)) as Hex21 by (apply hex_subst ; try assumption ; apply hex_nXX). assert (hex (subst (¬XX) XX h1 h2 f14)) as Hex22 by (apply hex_subst ; try assumption ; apply hex_nXX). rewrite (value_inj (subst (¬XX) YY h1 h2 (f13 ∨ f14)) (dual (rwedge (dual (subst (¬XX) YY h1 h2 f13)) (dual (subst (¬XX) YY h1 h2 f14)) (hex_dual _ Hex11) (hex_dual _ Hex12))) _ (hex_dual _ (hex_rwedge _ _ _ _))). rewrite (value_inj (subst (¬XX) XX h1 h2 (f13 ∨ f14)) (dual (rwedge (dual (subst (¬XX) XX h1 h2 f13)) (dual (subst (¬XX) XX h1 h2 f14)) (hex_dual _ Hex21) (hex_dual _ Hex22))) _ (hex_dual _ (hex_rwedge _ _ _ _))). rewrite (value_dual _ (hex_rwedge (¬(subst (¬XX) YY h1 h2 f13)) (¬(subst (¬XX) YY h1 h2 f14)) (hex_dual (subst (¬XX) YY h1 h2 f13) Hex11) (hex_dual (subst (¬XX) YY h1 h2 f14) Hex12))). rewrite (value_dual _ (hex_rwedge (¬(subst (¬XX) XX h1 h2 f13)) (¬(subst (¬XX) XX h1 h2 f14)) (hex_dual (subst (¬XX) XX h1 h2 f13) Hex21) (hex_dual (subst (¬XX) XX h1 h2 f14) Hex22))). assert (forall a b, a = b -> vneg a = vneg b) as Hv by (intros ; rewrite H ; reflexivity). apply Hv. { apply rwedge_preciseness. - rewrite (value_inj (dual (subst (¬XX) YY h1 h2 f13)) (dual (subst (¬XX) YY h1 h2 f13)) (hex_dual _ Hex11) (hex_dual _ (hex_subst h1 h2 f13 Hhh Hf1 (¬XX) YY hex_nXX hex_YY)) (OL_equiv_refl _)). rewrite (value_inj (dual (subst (¬XX) XX h1 h2 f13)) (dual (subst (¬XX) XX h1 h2 f13)) (hex_dual _ Hex21) (hex_dual _ (hex_subst h1 h2 f13 Hhh Hf1 (¬XX) XX hex_nXX hex_XX)) (OL_equiv_refl _)). rewrite (value_dual _ (hex_subst h1 h2 f13 Hhh Hf1 (¬XX) YY hex_nXX hex_YY)). rewrite (value_dual _ (hex_subst h1 h2 f13 Hhh Hf1 (¬XX) XX hex_nXX hex_XX)). apply Hv. apply IHf1. - rewrite (value_inj (dual (subst (¬XX) YY h1 h2 f14)) (dual (subst (¬XX) YY h1 h2 f14)) (hex_dual _ Hex12) (hex_dual _ (hex_subst h1 h2 f14 Hhh Hf2 (¬XX) YY hex_nXX hex_YY)) (OL_equiv_refl _)). rewrite (value_inj (dual (subst (¬XX) XX h1 h2 f14)) (dual (subst (¬XX) XX h1 h2 f14)) (hex_dual _ Hex22) (hex_dual _ (hex_subst h1 h2 f14 Hhh Hf2 (¬XX) XX hex_nXX hex_XX)) (OL_equiv_refl _)). rewrite (value_dual _ (hex_subst h1 h2 f14 Hhh Hf2 (¬XX) YY hex_nXX hex_YY)). rewrite (value_dual _ (hex_subst h1 h2 f14 Hhh Hf2 (¬XX) XX hex_nXX hex_XX)). apply Hv. apply IHf2. } rewrite dual_rwedge_dual_is_vee... rewrite dual_rwedge_dual_is_vee... Qed. Lemma context_preciseness_top : forall h1 h2 f, h1 <> h2 -> bicontext h1 h2 f -> subst (¬XX) XX h1 h2 f ≡ top -> subst (¬XX) YY h1 h2 f ≡ top . Proof. intros h1 h2 f Hhh Hf H. assert (value (subst (¬XX) XX h1 h2 f) (hex_subst h1 h2 f Hhh Hf (dual XX) XX hex_nXX hex_XX) = value top hex_top) as HXX by (apply value_inj ; assumption). assert (value (subst (¬XX) YY h1 h2 f) (hex_subst h1 h2 f Hhh Hf (dual XX) YY hex_nXX hex_YY) = value top hex_top) as HYY by (rewrite <- HXX ; apply rcontext_preciseness). destruct (hex_subst h1 h2 f Hhh Hf (¬XX) YY hex_nXX hex_YY) as [[[[[Hex | Hex] | Hex] | Hex] | Hex] | Hex] ; try assumption ; try (simpl in HYY ; inversion HYY). Qed. (* Proposition 4.2 *) Proposition no_diagonal : forall h1 h2 f, h1 <> h2 -> bicontext h1 h2 f -> ~ forall A B, ⊦ subst A B h1 h2 f, subst A B h1 h2 f <-> ⊦ A, B . Proof with try assumption. intros h1 h2 f Hhh Hf H. assert (H':= proj2 (H (¬ XX) XX)). assert (Hax:=@ax_ol (fun _ => True) (fun _ => True) (fun _ => True) XX I). apply H' in Hax. eapply (cw_ol _ bot) in Hax ; try apply I. assert (OL_equiv (subst (¬XX) XX h1 h2 f) top) as Htop. { split. - apply ex_ol. apply top_ol. - apply ex_ol... } apply context_preciseness_top in Htop... destruct Htop as [_ HYY]. assert (⊦ dual bot, subst (¬XX) YY h1 h2 f) as H'' by apply top_ol. apply ex_ol in HYY. apply (cut_elim_ol _ _ _ HYY) in H''. apply (proj1 (H _ _)) in H''. apply unprov_nXX_YY. apply ol_iff_olf... Qed. (* Proposition 4.3, Fact 1 *) Lemma not_var_var_rr_olf : forall x y, ~ olf rr (var x) (var y) . Proof. intros x y pi. apply (olf_is_polf plus) in pi. destruct pi as [l pi]. apply polf_to_ol in pi. apply not_var_var_ol in pi. assumption. Qed. (* Proposition 4.3, Fact 2 *) Lemma not_covar_covar_rr_olf : forall x y, ~ olf rr (covar x) (covar y) . Proof. intros x y pi. apply (olf_is_polf plus) in pi. destruct pi as [l pi]. apply polf_to_ol in pi. apply not_covar_covar_ol in pi. assumption. Qed. (* Proposition 4.3, Fact 3 *) Lemma not_bot_bot_rr_olf : ~ olf rr bot bot . Proof. intro pi. apply (olf_is_polf plus) in pi. destruct pi as [l pi]. apply polf_to_ol in pi. apply not_bot_bot_ol in pi. assumption. Qed. (* Proposition 4.3, Fact 4 *) Lemma top_top_olf : olf rr top top . Proof. apply top_rr_olf. Qed. (* Proposition 4.3, Fact 5 *) Lemma diag_wedge_olf : forall A B, olf rr A A /\ olf rr B B <-> olf rr (wedge A B) (wedge A B) . Proof. intros A B. rewrite_all <- ol_iff_olf. split. - intros [pi1 pi2]. apply wedge_ol ; apply cw_ol ; try assumption ; apply I. - intro pi. apply revert_wedge_ol_basic in pi. destruct pi as [pil pir]. apply ex_ol in pil. apply revert_wedge_ol_basic in pil. apply ex_ol in pir. apply revert_wedge_ol_basic in pir. split. + apply pil. + apply pir. Qed. (* Proposition 4.3, Fact 6 *) Lemma diag_vee_olf : forall A B, olf fc (vee A B) (vee A B) <-> olf rr (vee A B) (vee A B) . Proof with try assumption. intros A B. split ; intro pi. - apply cw_rr_olf... - inversion pi... inversion H... Qed. (* formula contains bot or var or covar below wedges only *) Inductive wedge_of_bot_at : formula -> Prop := | wba_var : forall x, wedge_of_bot_at (var x) | wba_covar : forall x, wedge_of_bot_at (covar x) | wba_bot : wedge_of_bot_at bot | wba_wedge_l : forall A B, wedge_of_bot_at A -> wedge_of_bot_at (wedge A B) | wba_wedge_r : forall A B, wedge_of_bot_at A -> wedge_of_bot_at (wedge B A) . (* wedge_of_bot_at is a decidable property *) Lemma wedge_of_bot_at_dec : forall A, {wedge_of_bot_at A} + {~ wedge_of_bot_at A} . Proof with try assumption. induction A ; try (now left ; constructor) ; try (now right ; intro Hw ; inversion Hw ). destruct IHA1 ; destruct IHA2 ; try (now left ; constructor ; assumption). - left. apply wba_wedge_r... - right. intro Hw. inversion Hw ; subst. + apply n... + apply n0... Qed. (* End of Section 4.2, Part 1 *) Lemma not_diag_olf : forall A, wedge_of_bot_at A -> ~ olf rr A A . Proof with try eassumption. induction A ; intros Hw pi. - eapply not_var_var_rr_olf... - eapply not_covar_covar_rr_olf... - inversion Hw. - eapply not_bot_bot_rr_olf... - inversion Hw. + apply IHA1... apply diag_wedge_olf in pi... apply pi. + apply IHA2... apply diag_wedge_olf in pi... apply pi. - inversion Hw. Qed. (* End of Section 4.2, Part 2 *) Lemma vee_for_diag_olf : forall A, ~ wedge_of_bot_at A -> exists f p, (forall n, n < p -> subform (f n) A /\ is_vee (f n)) /\ ((olf rr A A) <-> forall n, n < p -> olf fc (f n) (f n)) . Proof with try assumption ; try (now constructor) ; try omega. induction A ; intro Hw ; try (now exfalso ; apply Hw ; constructor). - exists (fun _ => bot). exists 0. split ; [ | split]. + intros n Hn... + intros... + intros. apply top_rr_olf... - assert (~ wedge_of_bot_at A1) as Hw1 by (intro Hw1 ; apply Hw ; apply wba_wedge_l ; assumption). assert (~ wedge_of_bot_at A2) as Hw2 by (intro Hw2 ; apply Hw ; apply wba_wedge_r ; assumption). destruct (IHA1 Hw1) as [f1 [p1 H1]]. destruct (IHA2 Hw2) as [f2 [p2 H2]]. exists (fun n => if (leb (S n) p1) then f1 n else f2 (n - p1)). exists (p1 + p2). split ; [ | split ]... + intros n Hn. case_bool (S n) p1. * assert (n < p1)... destruct H1 as [H1 _]. apply H1 in H. destruct H as [Hs Hv]. split... * assert (n - p1 < p2)... destruct H2 as [H2 _]. apply H2 in H. destruct H as [Hs Hv]. split... apply sub_wedge_r... + intros Hex n Hn. case_bool (S n) p1. * assert (n < p1)... destruct H1 as [_ H1]. apply H1 in H... apply diag_wedge_olf in Hex. apply Hex. * assert (n - p1 < p2)... destruct H2 as [_ H2]. apply H2 in H... apply diag_wedge_olf in Hex. apply Hex. + intros Hex. apply diag_wedge_olf. split. * apply H1. intros n Hn. assert (S n <= p1) as Hn'... apply leb_correct in Hn'. specialize Hex with n. assert (n < p1 + p2) as Hnp... apply Hex in Hnp. rewrite Hn' in Hnp... * apply H2. intros n Hn. assert (p1 < S (p1 + n)) as Hn'... apply leb_correct_conv in Hn'. specialize Hex with (p1 + n). assert (p1 + n < p1 + p2) as Hnp... apply Hex in Hnp. rewrite Hn' in Hnp... assert (p1 + n - p1 = n)... rewrite H in Hnp... - exists (fun _ => vee A1 A2). exists 1. split ; split... + intros Hex n Hn. inversion Hex... inversion H... + intro Hex. specialize Hex with 0. assert (0 < 1) as pi... apply Hex in pi. eapply cw_rr_olf... Qed. (** Forward Proof Search **) Inductive sv_subform : formula -> formula -> Prop := | sv_sub_vee_l_id : forall A B, sv_subform A (vee A B) | sv_sub_vee_r_id : forall A B, sv_subform A (vee B A) | sv_sub_vee_l : forall A B C, sv_subform A B -> sv_subform A (vee B C) | sv_sub_vee_r : forall A B C, sv_subform A B -> sv_subform A (vee C B) | sv_sub_wedge_l : forall A B C, sv_subform A B -> sv_subform A (wedge B C) | sv_sub_wedge_r : forall A B C, sv_subform A B -> sv_subform A (wedge C B) . Lemma sv_subform_trans : forall B C, subform B C -> forall A, sv_subform A B -> sv_subform A C . Proof with try assumption. intros B C Hs. induction Hs ; intros A0 Hs0 ; try apply IHHs in Hs0... - apply sv_sub_vee_l... - apply sv_sub_vee_r... - apply sv_sub_wedge_l... - apply sv_sub_wedge_r... Qed. Inductive sw_subform : formula -> formula -> Prop := | sw_sub_wedge_l_id : forall A B, sw_subform A (wedge A B) | sw_sub_wedge_r_id : forall A B, sw_subform A (wedge B A) | sw_sub_vee_l : forall A B C, sw_subform A B -> sw_subform A (vee B C) | sw_sub_vee_r : forall A B C, sw_subform A B -> sw_subform A (vee C B) | sw_sub_wedge_l : forall A B C, sw_subform A B -> sw_subform A (wedge B C) | sw_sub_wedge_r : forall A B C, sw_subform A B -> sw_subform A (wedge C B) . Lemma sw_subform_trans : forall B C, subform B C -> forall A, sw_subform A B -> sw_subform A C . Proof with try assumption. intros B C Hs. induction Hs ; intros A0 Hs0 ; try apply IHHs in Hs0... - apply sw_sub_vee_l... - apply sw_sub_vee_r... - apply sw_sub_wedge_l... - apply sw_sub_wedge_r... Qed. Definition subformseq t A B R := (subform A R /\ subform B R) /\ ((t = rv \/ t = fc) -> sync A -> A = R \/ sw_subform A R) /\ (t = rv -> sync B -> sw_subform B R) /\ (t = fc -> async B -> sv_subform B R) . Ltac subformseq_decomp := unfold subformseq ; (split ; [ split | split ; [ | split ]]) ; try (now intro Ht ; inversion Ht) ; try assumption ; try intro Ht . Ltac subformseq_simpl H := inversion H as [[Pss1 Pss2] [Pss3 [Pss4 Pss5]]] ; subformseq_decomp . Lemma forget_strong_sub_formula : forall fs R t A B l, @polf (fun t' A' B' => subformseq t' A' B' R) fs t A B l -> @polf (fun _ _ _ => True) fs t A B l . Proof with try eassumption ; try now apply I. intros fs R t A B l pi. induction pi ; try (now constructor ; try (now apply I) ; apply IHpi). - apply vee_r_fc_polf... - apply top_rv_polf... - apply wedge_rv_polf... - apply wedge_rr_polf... - apply unfoc_fc_polf... - apply foc_l_rv_polf... - apply foc_r_rv_polf... - apply cw_rr_polf... - apply cw_rv_polf... Qed. Proposition strong_sub_formula : forall fs R t A B l, t <> rr -> @polf (fun _ _ _ => True) fs t A B l -> subformseq t A B R -> @polf (fun t' A' B' => subformseq t' A' B' R) fs t A B l . Proof with try eassumption ; try (now constructor) ; try (now intro Hseq ; inversion Hseq). intros fs R t A B l Hrr pi. induction pi ; intro Pss ; try (constructor ; eassumption) ; try (now destruct Hrr ; constructor)... - apply vee_l_fc_polf... apply IHpi... subformseq_simpl Pss. + eapply subform_trans... apply sub_vee_l... + intro Ha. eapply sv_subform_trans... - apply vee_r_fc_polf... apply IHpi... subformseq_simpl Pss. + eapply subform_trans... apply sub_vee_r... + intro Ha. eapply sv_subform_trans... - apply wedge_rv_polf... + apply IHpi1... subformseq_simpl Pss. * eapply subform_trans... apply sub_wedge_l... * intro Hs. eapply sw_subform_trans... + apply IHpi2... subformseq_simpl Pss. * eapply subform_trans... apply sub_wedge_r... * intro Hs. eapply sw_subform_trans... - apply unfoc_fc_polf... apply IHpi... subformseq_simpl Pss. + apply Pss3. right... + intro Hs ; inversion H0 ; subst ; inversion Hs. - apply foc_l_rv_polf... apply IHpi... subformseq_simpl Pss. + intro Hs. right. apply Pss4... + intro Ha ; inversion Ha ; subst ; inversion H0. - apply foc_r_rv_polf... apply IHpi... subformseq_simpl Pss. + apply Pss3. left... + intro Ha ; inversion Ha ; subst ; inversion H0. - apply cw_rv_polf... apply IHpi... subformseq_simpl Pss. intros. right. apply Pss4... Qed. Notation "l ⊦⊦ A ⇓ B" := (@polf (fun t' A' B' => subformseq t' A' B' A) max fc A B l) (at level 50). (* Proposition 4.4 *) Proposition strong_sub_formula_diag : forall B C l, l ⊦⊦ B ∨ C ⇓ B ∨ C <-> l ⊦ B ∨ C ⇓ B ∨ C . Proof. intros A l. split. - apply forget_strong_sub_formula. - intro pi. eapply strong_sub_formula in pi. + eassumption. + intro Hfc. inversion Hfc. + subformseq_decomp ; try apply sub_id ; intros. left ; reflexivity. Qed. (* Automatic Backward Proof Search Tactic *) Ltac oauto := intros ; (try apply ax_fc_olf) || (try (now apply vee_l_fc_olf ; oauto)) || (try (now apply vee_r_fc_olf ; oauto)) || (try (now apply top_rv_olf ; try auto_sync_async)) || (try apply top_rr_olf) || (try (now apply wedge_rv_olf ; oauto)) || (try (now apply wedge_rr_olf ; oauto)) || (try (apply unfoc_fc_olf ; [ now try auto_sync_async | now oauto ])) || (try (now apply unrev_rr_olf ; oauto)) || (try (apply foc_l_rv_olf ; [ now try auto_sync_async | now oauto ])) || (try (apply foc_r_rv_olf ; [ now try auto_sync_async | now oauto ])) || (try (now apply cw_rr_olf ; oauto)) || (try (apply cw_rv_olf ; [ now try auto_sync_async | now oauto ])) . (* Example 3.12 *) Example example_1_3_oauto : forall x y, ⊦ ⇑ ⊥, ((ν x ∧ ν y) ∨ κ x) ∨ κ y . Proof. oauto. Qed. Goal forall x, ⊦ ⇑ ν x, κ x. Proof. oauto. Qed. Goal forall x, ⊦ ⇑ ν x ∨ κ x, ν x ∨ κ x. Proof. oauto. Qed. Goal forall x, ⊦ ⇑ ν x ∨ κ x, ⊥. Proof. oauto. Qed. Goal forall x, ⊦ ⇑ ⊥, ν x ∨ κ x. Proof. oauto. Qed. Goal forall x a b c d, ⊦ ⇑ (ν x ∨ a) ∨ b, (c ∨ (d ∨ κ x)) ∧ ⊤. Proof. oauto. Qed. Goal forall x y z t, ⊦ ⇑ ((ν x ∧ ν y) ∧ (ν x ∧ ν z)) ∨ (((κ x ∧ (ν t ∨ κ t)) ∨ κ y) ∨ κ z), ((ν x ∧ ν y) ∧ (ν x ∧ ν z)) ∨ (((κ x ∧ (ν t ∨ κ t)) ∨ κ y) ∨ κ z). Proof. oauto. Qed. Goal forall x y, ⊦ ⇑ ⊥, ((ν y ∨ κ y) ∧ ν x) ∨ κ x. Proof. oauto. Qed.