(* Developed under The Coq Proof Assistant version 8.4pl1 *) (* with some unicode notations *) (* https://coq.inria.fr/ *) Require Import NPeano. Require Import Coq.Setoids.Setoid. Require Import Coq.Program.Equality. 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 with simpl ; omega. induction n... Qed. Lemma exp_mon : forall n m, n <= m -> exp n <= exp m . Proof with try (simpl ; lia). intros n m H. induction H... 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)... rewrite H... - assert (m <= n) as Ho... assert (Hf := Hmon _ _ Ho). assert (max m n = n)... rewrite H... 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. (* Finite Axiom of Choice *) (* Functional Axiom of Choice for finite function *) 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 assumption ; 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 by omega. 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... Qed. (* Pre-Orders and Lattices Hierarchy *) Class PreOrder {T:Type} := { leq : T -> T -> Prop; refl : forall x, leq x x; trans : forall x y z, leq x y -> leq y z -> leq x z }. Class PreLattice {T:Type} := { isorder :> PreOrder; 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:Type} := { islattice :> PreLattice; 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 *) Class PreOrthoLattice {T:Type} := { isinvollattice :> PreInvolLattice (T:=T); compl : forall x, leq te (sup x (perp x)) }. (* Example 2 *) Example example2 {T:Type} {OL:PreOrthoLattice (T:=T)} : forall x y, leq te (sup (sup (inf x y) (perp x)) (perp y)) . Proof. intros x y. eapply trans. - eapply trans. + apply compl. + apply sup_leq. * apply sup_geq1. * (* 1 *) { eapply trans. - eapply trans. + apply contrap. apply inf_geq. * eapply trans. apply contrap. apply sup_geq1. apply invol_leq. * eapply trans. apply contrap. apply sup_geq2. apply invol_leq. + apply invol_leq. - apply sup_geq2. } - (* 2 *) { apply sup_leq. - eapply trans. + apply sup_geq1. + apply sup_geq1. - apply sup_leq. + eapply trans. * 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 : formula := 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 with try reflexivity. induction A ; simpl ; (try reflexivity) ; rewrite IHA1 ; rewrite IHA2... 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 : nat := 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 with try reflexivity. induction A ; simpl ; (try reflexivity) ; rewrite IHA1 ; rewrite IHA2... 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 E]]. 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 (left ; constructor ; fail) ; try (right ; constructor ; fail). Qed. Lemma async_dual : forall A, async (dual A) <-> sync A . Proof. intro A ; split ; induction A ; intro Hs ; simpl ; try (inversion Hs ; fail) ; constructor. Qed. Lemma sync_dual : forall A, sync (dual A) <-> async A . Proof. intro A ; split ; induction A ; intro Hs ; simpl ; try (inversion Hs ; fail) ; 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) | _ => assumption ; fail end. (** System OL **) (* Definition of OL *) (* pax pctr and pwk are parameters for variants of the system *) 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, not (@ol pax pctr pwk (var x) (var y)) . Proof. intros x y pax pctr pwk pi. dependent induction pi ; assumption. Qed. Lemma not_covar_covar_ol : forall x y pax pctr pwk, not (@ol pax pctr pwk (covar x) (covar y)) . Proof. intros x y pax pctr pwk pi. dependent induction pi ; assumption. Qed. Lemma not_bot_bot_ol : forall pax pctr pwk, not (@ol pax pctr pwk bot bot) . Proof. intros pax pctr pwk H. dependent induction H ; assumption. Qed. (* Lemma 9 *) 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) ). { intros A B pax pctr pwk Hpax Hpctr Hpwk HI. induction HI ; (split ; [idtac | 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 (constructor ; fail) ; try (apply (IH A1 A2)) ; try (apply (Hpctr A1 A2) ; subst)... - intros B1 B2 HB. split ; apply cw_ol ; try (constructor ; fail) ; 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 H in Hw... destruct Hw as [H2 _]. apply H2... 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 ax_var_ol : forall x, ⊦ κ x, ν x . Proof with try (constructor ; fail). intro x. assert (covar x = dual (var x)) as Hc by (simpl ; reflexivity). rewrite Hc. apply ax_ol... Qed. (* Example 7 *) Example example2_ol : forall x y, ⊦ bot , vee (vee (wedge (var x) (var y)) (covar x)) (covar y) . Proof with try (constructor ; fail). intros x y. apply ex_ol. apply cw_ol... 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 8 *) Proposition ax_exp_ol : forall A, α⊦ (dual A), A . Proof with try assumption ; try (apply ex_ol ; assumption). induction A ; try (simpl ; constructor ; fail) ; try (apply ex_ol ; constructor ; fail). - 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 assumption. intros A B. split ; intro H ; induction H ; try (constructor ; assumption ; fail). + apply ax_exp_ol. + apply vee_r_ol... + apply ex_ol... + apply ax_ol. constructor. + apply vee_r_ol... + apply ex_ol... Qed. (* Lemma 10, part 1 *) Lemma vee_ctr_ol : forall A B, τ⊦ A, A -> τ⊦ A, B . Proof with assumption. induction A ; intros B H. - apply not_var_var_ol in H. exfalso... - apply not_covar_covar_ol in H. exfalso... - apply top_ol. - apply not_bot_bot_ol in H. exfalso... - 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 ; constructor. } { 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 ; constructor. } + intros D E Hv. destruct Hv as [Hv | Hv] ; inversion Hv. + intros D E Hw ; inversion Hw. + intros ; split ; constructor. - apply cw_ol ; try (constructor ; fail)... Qed. Lemma vee_ol : forall A B, α⊦ A , B <-> τ⊦ A , B . Proof with assumption. intros A B. split ; intro H ; induction H ; try (constructor ; assumption ; fail). - apply vee_r_ol... - apply vee_ctr_ol... - apply ex_ol... - apply vee_r_ol... - apply ex_ol... Qed. (* Lemma 10, 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 (apply cw_ol ; try assumption ; try (left ; constructor) ; try (right ; constructor) ; fail). - 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 (constructor ; assumption ; fail). - apply vee_r_ol... - apply sync_wk_ol... - apply ex_ol... - apply vee_r_ol... - apply cw_ol... constructor. - 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 11 *) 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 ; [idtac | 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... - destruct eq... - destruct 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 with assumption. intros C A l pi. apply left_is_sync_or_covar_fc_olf0 in pi. setoid_rewrite sync_dual in pi. setoid_rewrite is_covar_dual in pi... 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 with assumption. intros C A l pi. apply left_is_sync_or_covar_rv_olf0 in pi. setoid_rewrite sync_dual in pi. setoid_rewrite is_covar_dual in pi... 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 with assumption. 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... Qed. (* Example 12 *) 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. (* Proposition 13 *) 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 (constructor ; fail). intros t A B l pi. dependent induction pi ; try (constructor ; assumption ; fail) ; try (apply ex_ol ; constructor ; assumption ; fail) ; try (apply ex_ol ; constructor ; apply ex_ol ; assumption ; fail)... - apply ax_var_ol. - apply ex_ol. apply vee_r_ol... - apply cw_ol... - apply ex_ol. apply cw_ol... Qed. (* End of Section 3.1 Fact 1 *) Lemma not_var_var_ll_olf0 : forall x y l, not (olf0 ll4 (var x) (var y) l) . Proof. intros x y l pi. dependent induction pi ; try (inversion pi ; inversion H0 ; fail) ; try destruct IHpi. Qed. (* End of Section 3.1 Fact 2 *) Lemma not_covar_covar_ll_olf0 : forall x y l, not (olf0 ll4 (covar x) (covar y) l) . Proof. intros x y l pi. dependent induction pi ; try (inversion H ; fail) ; try inversion IHpi. Qed. (* End of Section 3.1 Fact 3 *) Lemma not_bot_bot_ll_olf0 : forall l, not (olf0 ll4 bot bot l) . Proof. intros l pi. dependent induction pi ; try (inversion pi ; inversion H0 ; fail) ; try (inversion IHpi). Qed. (* End of Section 3.1 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. dependent induction pi. - apply foc_r_ll_olf0... - apply foc_l_ll_olf0... - apply cw_r_ll_olf0... - apply cw_l_ll_olf0... Qed. (* End of Section 3.1 Fact 5 *) Lemma foc_biform_olf0 : forall A l, olf0 ll4 A A l -> exists l', olf0 fc4 A A l' /\ l' < l . Proof. intros A l pi. dependent induction pi ; try (eexists ; split ; try eassumption ; try omega ; fail) ; try (destruct IHpi as [l' [Heq IH]] ; eexists ; split ; try eassumption ; try omega ; fail). Qed. (* Cut Elimination *) (* Theorem 14, 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 14, 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 14, 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 (unfold lt_nat_nat ; simpl ; left ; omega ; fail) ; try (unfold lt_nat_nat ; simpl ; right ; split ; omega ; fail) ; 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 ; [idtac | split ; [idtac | split ; [idtac | 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... - assert (Hs := H0). apply left_is_async_or_var_ll_olf0 in Hs. inversion Hs. + simpl in H4. assert (pi1' := pi1). apply foc_biform_olf0 in H0. destruct H0 as [l3 [pi3 Hl3]]. 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 H4 ; inversion H2. - apply IH with (1,l0) _ _ _ in pi1'... + destruct pi1' as [_ [_ [pi1' _]]]. apply (pi1' C) in H4... destruct H4 as [l4 pi4]. eexists. apply foc_r_ll_olf0... + unfold lt_nat_nat ; simpl in Hsize ; simpl... - apply not_bot_bot_ll_olf0 in H4 ; destruct H4. - eexists. apply cw_r_ll_olf0... } * simpl in Hsize. inversion pi3 ; subst. assert (Has := sync_or_async A0). inversion Has. { rewrite <- bidual in H3. inversion H6 ; subst ; try (rewrite <- H4 in H3 ; simpl in H3 ; inversion H3 ; fail). apply IH with (fsize A0,l4) _ _ _ in H5... destruct H5 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 H6... destruct H6 as [l6 pi6]. eexists. apply cw_l_ll_olf0... } assert (Has := sync_or_async B0). inversion Has. { rewrite <- bidual in H3. inversion H6 ; subst ; try (rewrite <- H4 in H3 ; simpl in H3 ; inversion H3 ; fail). apply IH with (fsize B0,l5) _ _ _ in H5... destruct H5 as [pi4 _]. rewrite bidual in pi4. apply (pi4 A) in H2... destruct H2 as [l6 pi6]. eexists. apply cw_l_ll_olf0... } { apply IH with (fsize B0,l1) _ _ _ in H2... destruct H2 as [_ [_ [_ [pi4 _]]]]. apply (pi4 A) in H6... destruct H6 as [l6 pi6]. eexists. apply cw_l_ll_olf0... } simpl in H3. inversion H3. * assert (H2 := H0). apply left_is_sync_or_covar_ll_olf0 in H0. inversion H0. destruct B ; try (inversion H1 ; fail) ; try (inversion H3 ; fail). inversion H3 ; subst. eapply cut_elim_v_1_olf0 in pi2... destruct pi2 as [l pi2]. eexists. apply ex_ll_olf0... + inversion H1 ; subst. eapply not_covar_covar_ll_olf0 in H0... (* 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 (inversion H ; fail). 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 (inversion H ; fail). 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 (inversion H1 ; fail) ; try (inversion H ; fail). + 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 14, 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. dependent induction pi1 ; 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 14, 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. dependent induction pi1 ; 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 15, part 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 15, part 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 15, part 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 15, part 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. dependent induction pi. - apply top_r_rr_olf0. - destruct IHpi1 as [l1' IH1]. destruct IHpi2 as [l2' IH2]. eapply wedge_r_rr_olf0... - eapply unrev_l_rr_olf0... Qed. (* Lemma 16, 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 eassumption ; 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... - eexists. apply unrev_rv_olf0. apply foc_l_ll_olf0... apply vee_r_fc_olf0. apply unfoc_fc_olf0... Qed. (* Lemma 16, part 2 *) Lemma vee_l_sync_olf0 : forall l t A C B, olf0 t A C l -> not (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 (destruct Ht ; reflexivity ; fail). - 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 [l1' [pi' Hleq]]. 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 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. * assumption. * assumption. + inversion H1 ; subst. inversion pi'. inversion H3. eapply not_covar_covar_ll_olf0 in H4... - split ; eexists ; apply cw_r_ll_olf0... + eassumption. + eassumption. Qed. (* Proposition 17 *) 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 18 *) 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. dependent 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 (inversion H ; fail). inversion H1 ; subst ; try (inversion H ; fail). 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 19 *) 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 any ortholattice *) Fixpoint f2o {T:Type} {IL:PreInvolLattice} (r : Atom -> T) (A : formula) : 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:Type} {IL:PreInvolLattice (T:=T)} : leq (perp te) be /\ leq be (perp te) . Proof. split. - eapply trans. + apply contrap. apply te_geq. + apply invol_leq. - apply be_leq. Qed. Lemma dual_bot_valid {T:Type} {IL:PreInvolLattice (T:=T)} : leq (perp be) te /\ leq te (perp be) . Proof. split. - apply te_geq. - eapply trans. + apply invol_geq. + apply contrap. apply be_leq. Qed. Lemma dual_wedge_valid {T:Type} {IL:PreInvolLattice (T:=T)} : 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 trans. + apply contrap. apply inf_geq. * eapply trans. apply contrap. apply sup_geq1. apply invol_leq. * eapply trans. 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:Type} {IL:PreInvolLattice (T:=T)} : 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 trans. + apply invol_geq. + apply contrap. apply sup_leq. * eapply trans. apply invol_geq. apply contrap. apply inf_leq1. * eapply trans. apply invol_geq. apply contrap. apply inf_leq2. Qed. Lemma f2o_dual {T:Type} {IL:PreInvolLattice (T:=T)}: 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 refl. - split. + apply invol_leq. + apply invol_geq. - apply dual_top_valid. - apply dual_bot_valid. - destruct IHA1. destruct IHA2. split. + eapply trans. * apply dual_wedge_valid. * apply sup_leq. eapply trans. apply H. apply sup_geq1. eapply trans. 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 dual_wedge_valid. apply sup_leq. eapply trans. apply H0. apply contrap. apply inf_leq1. eapply trans. apply H2. apply contrap. apply inf_leq2. - destruct IHA1. destruct IHA2. split. + eapply trans. apply dual_vee_valid. apply inf_geq. * eapply trans. apply inf_leq1. assumption. * eapply trans. 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 dual_vee_valid. eapply trans ; try eassumption. apply inf_geq. eapply trans. apply inf_leq1. assumption. eapply trans. apply inf_leq2. assumption. Qed. Lemma ex_valid {T:Type} {IL:PreInvolLattice (T:=T)} : forall A B, leq (perp A) B -> leq (perp B) A . Proof. intros A B pi. apply trans with (perp (perp A)). - apply contrap. assumption. - apply invol_leq. Qed. Lemma top_valid {T:Type} {IL:PreInvolLattice (T:=T)} : forall A, leq (perp te) A . Proof. intros. eapply trans. - apply dual_top_valid. - apply be_leq. Qed. Lemma wedge_valid {T:Type} {IL:PreInvolLattice (T:=T)} : forall A B C, leq (perp A) C -> leq (perp B) C -> leq (perp (inf A B)) C . Proof with assumption. intros A B C pi1 pi2. apply contrap. eapply trans ; [idtac | apply invol_geq]. apply inf_geq ; apply ex_valid... Qed. Lemma vee_l_valid {T:Type} {IL:PreInvolLattice (T:=T)} : forall A C B, leq (perp A) C -> leq (perp (sup A B)) C . Proof. intros A C B pi. eapply trans. - apply contrap. apply sup_geq1. - assumption. Qed. Lemma vee_r_valid {T:Type} {IL:PreInvolLattice (T:=T)} : forall A C B, leq (perp A) C -> leq (perp (sup B A)) C . Proof. intros A C B pi. eapply trans. - apply contrap. apply sup_geq2. - assumption. Qed. Lemma cw_valid {T:Type} {OL:PreOrthoLattice (T:=T)} : forall A B, leq (perp A) A -> leq (perp A) B . Proof with try eassumption. intros A B pi. apply trans with (inf A (perp A)). - apply inf_geq... apply refl. - eapply trans. + apply contrap. eapply trans. * apply dual_bot_valid. * eapply trans. apply compl. apply dual_wedge_valid. + apply be_leq. Qed. (* Theorem 6 o Theorem 5 Part 1 *) Theorem ol_to_ord {T:Type} {OL:PreOrthoLattice (T:=T)} : forall r A B, ⊦ A , B -> leq (perp (f2o r A)) (f2o r B) . Proof with assumption. intros r A B pi. dependent induction pi ; simpl. - 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 *) Instance OL_PreOrder : PreOrder (T:=formula). Proof with try eassumption ; try (constructor ; fail). split with (fun A B => ⊦ (dual A), B). - intro A. apply ax_ol... - intros A B C pi1 pi2. eapply cut_elim_ol... Defined. Instance OL_PreLattice : PreLattice (T:=formula). Proof with try (constructor ; fail) ; try assumption. split with OL_PreOrder vee wedge top bot ; try (intros A B C) ; try (intros A B) ; try intro A. - 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. Instance OL_InvolLattice : PreInvolLattice (T:=formula). Proof with assumption. split with OL_PreLattice dual. - intro A. rewrite bidual. apply refl. - intro A. rewrite bidual. apply refl. - intros A B. split. + intro pi. apply ex_ol. unfold leq in pi. simpl in pi. rewrite bidual in pi... + intro pi. simpl. rewrite bidual. apply ex_ol... Defined. Instance OL_OrthoLattice : PreOrthoLattice (T:=formula). Proof with try (constructor ; fail). 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 6 o Theorem 5 Part 2 *) Theorem ord_to_ol : forall A B, (forall OL:PreOrthoLattice (T:=formula), leq A B) -> ⊦ (dual A) , B . Proof. intros A B Ho. apply Ho. apply OL_OrthoLattice. 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 20 *) Example example2_olf : forall x y, olf rr 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 use to constrain internal sequents with a predicate, fs is used for computing size in binary rules: typically + or max 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 (constructor ; fail) ; try eassumption ; try auto_sync_async. intros fs t A B. split. - intro pi. induction pi ; try (eexists ; constructor ; try (constructor ; fail) ; fail) ; try (destruct IHpi as [l pi'] ; eexists ; constructor ; try (constructor ; fail) ; try eassumption ; try auto_sync_async ; fail). + destruct IHpi as [l pi']. eexists. apply vee_r_fc_polf... + eexists ; constructor... + 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 (constructor ; try eassumption ; try auto_sync_async ; fail). + 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, not (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, not (l ⊦ A ⇓ bot) . Proof. intros A l pi. inversion pi. inversion H0 ; inversion H1. Qed. (* Proposition 21, 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 (auto_sync_async ; fail). intros t A B l pi. induction pi ; (split ; [idtac | split ; [idtac | split]]) ; intro Ht ; try (inversion Ht ; fail) ; try (eexists ; constructor ; assumption ; fail) ; try (eexists ; constructor ; constructor ; fail) ; try (left ; eexists ; constructor ; assumption ; fail) ; try (left ; eexists ; constructor ; [ constructor | assumption] ; fail) ; try (left ; eexists ; constructor ; constructor ; assumption ; fail). - 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 21, 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 22 *) 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 (constructor ; fail). intros Pss fs t A B l pi. dependent induction pi ; try (constructor ; assumption ; fail) ; try (apply ex_ol ; constructor ; assumption ; fail) ; try (apply ex_ol ; constructor ; apply ex_ol ; assumption ; fail)... - 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 Polf 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... - eapply olf_is_polf in pi. destruct pi as [l pi]. apply polf_to_ol in pi... Grab Existential Variables. apply plus. Qed. (** Backward Proof Search **) (* measure on formulas *) Fixpoint gsize A : nat := 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 : nat := 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 with try (simpl ; lia). intros. assert (Hs := gsize_pos C). case B ; intros... Qed. Fact f2 : forall A B C, ssize fc A B < ssize fc A (vee C B). Proof with try (simpl ; lia). intros. assert (Hs := gsize_pos C). case B ; intros... 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 with try (simpl ; lia). intros. destruct B ; try (inversion H as [Ha | Ha] ; inversion Ha ; fail)... Qed. Fact f6 : forall A B, ssize rv A B < ssize rr A B. Proof with try (simpl ; lia). intros. assert (He := gsize_pos A)... 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 (inversion H ; fail)... assert (Hs := gsize_pos B2)... Qed. Fact f8 : forall A B, sync B -> ssize fc A B < ssize rv B A. Proof with try (simpl ; lia). intros. assert (Hs := gsize_pos A). destruct B ; try (inversion H ; fail)... Qed. Fact f9 : forall A B, sync A -> ssize fc A A < ssize rr A B. Proof with try (simpl ; lia). intros. assert (Hs := gsize_pos B). destruct A ; try (inversion H ; fail)... Qed. Fact f10 : forall A B, sync A -> ssize fc A A < ssize rv B A. Proof with try (simpl ; lia). intros. assert (Hs := gsize_pos B). destruct A ; try (inversion H ; fail)... Qed. Fact f11 : forall A B C, ssize rr B A < ssize rr (wedge B C) A. Proof with try (simpl ; lia). intros. assert (Hs := gsize_pos C)... Qed. Fact f12 : forall A B C, ssize rr B A < ssize rr (wedge C B) A. Proof with try (simpl ; lia). intros. assert (Hs := gsize_pos C)... Qed. (* Proposition 23 *) 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 apply IHHs ; try assumption. intros B C Hs. induction Hs ; intros A0 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 (constructor ; fail) ; try (split ; assumption ; fail). 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 assumption ; try (constructor ; fail). intros fs t A B l pi. apply sub_formula_0... - 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 (eexists ; constructor ; fail) ; 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 with try (simpl ; omega). intros A B i Hs. induction Hs... 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 ; [ idtac | 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 ; [ idtac | 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 ; [ idtac | 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 ; [ idtac | split] ; intro Hl... - exists (fun n => rr). exists (fun n => top). exists (fun n => C). intro n. split ; [ idtac | split] ; intro Hl... - destruct (Nat.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 ; [ idtac | 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 ; [ idtac | 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 (Nat.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 ; [ idtac | 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 ; [ idtac | 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 ; [ idtac | 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 ; [ idtac | 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 ; [ idtac | 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 ; [ idtac | 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 ; [ idtac | 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 ; [ idtac | 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, ((forall t:seq_3, e t < 3) /\ (forall t1 t2, e t1 = e t2 -> t1 = t2)) . Proof with try reflexivity ; try omega. eexists (fun t => match t with fc => 0 | rv => 1 | rr => 2 end). split. - destruct t... - intros t1 t2. destruct t1 ; destruct t2... 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. { 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. { apply (uniq_euclid_divid _ (f1 (e1 m)) (fsize R1 + fsize R2) (f1 (e1 n)))... nia. } assert (f1 (e1 n) = f1 (e1 m)) as He1. { 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 **) (* Proposition 24, part 1 *) Lemma not_var_var_rr_olf : forall x y, not (olf rr (var x) (var y)) . Proof. intros x y pi. rewrite olf_is_polf in pi. destruct pi as [l pi]. apply polf_to_ol in pi. apply not_var_var_ol in pi. assumption. Grab Existential Variables. apply plus. Qed. (* Proposition 24, part 2 *) Lemma not_covar_covar_rr_olf : forall x y, not (olf rr (covar x) (covar y)) . Proof. intros x y pi. rewrite olf_is_polf in pi. destruct pi as [l pi]. apply polf_to_ol in pi. apply not_covar_covar_ol in pi. assumption. Grab Existential Variables. apply plus. Qed. (* Proposition 24, part 3 *) Lemma not_bot_bot_rr_olf : not (olf rr bot bot) . Proof. intro pi. rewrite olf_is_polf in pi. destruct pi as [l pi]. apply polf_to_ol in pi. apply not_bot_bot_ol in pi. assumption. Grab Existential Variables. apply plus. Qed. (* Proposition 24, part 4 *) Lemma top_top_olf : olf rr top top . Proof. apply top_rr_olf. Qed. (* Proposition 24, part 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 with try (constructor ; fail) ; try eassumption. intros A B. rewrite_all <- ol_iff_olf. split. - intros [pi1 pi2]. apply wedge_ol ; apply cw_ol... - intro pi. split. + eapply cut_elim_ol... * apply ex_ol. apply vee_l_ol. apply ax_ol... * simpl ; rewrite bidual. rewrite <- (bidual B) in pi. eapply cut_elim_ol... simpl. apply vee_l_ol. apply ax_ol... + eapply cut_elim_ol... * apply ex_ol. apply vee_r_ol. apply ax_ol... * simpl ; rewrite_all bidual. rewrite <- (bidual A) in pi. eapply cut_elim_ol... simpl. apply vee_r_ol. apply ax_ol... Qed. (* Proposition 24, part 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 \/ not (wedge_of_bot_at A) . Proof with try assumption. induction A ; try (left ; constructor ; fail) ; try (right ; intro Hw ; inversion Hw ; fail). destruct IHA1 ; destruct IHA2 ; try (left ; constructor ; assumption ; fail). - left. apply wba_wedge_r... - right. intro Hw. inversion Hw ; subst. + apply H... + apply H0... Qed. (* End of Section 4.2 Part 1 *) Lemma not_diag_olf : forall A, wedge_of_bot_at A -> not (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, not (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 (constructor ; fail) ; try omega. induction A ; intro Hw ; try (exfalso ; apply Hw ; constructor ; fail). - exists (fun _ => bot). exists 0. split ; [idtac | split]. + intros n Hn... + intros... + intros. apply top_rr_olf... - assert (not (wedge_of_bot_at A1)) as Hw1. { intro Hw1. apply Hw. apply wba_wedge_l... } assert (not (wedge_of_bot_at A2)) as Hw2. { intro Hw2. apply Hw. apply wba_wedge_r... } 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 ; [idtac | 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... apply sub_wedge_l... * 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 apply IHHs ; try assumption. intros B C Hs. induction Hs ; intros A0 Hs0... - apply sv_sub_vee_l... - apply sv_sub_vee_r... - apply sv_sub_wedge_l... - apply sv_sub_wedge_r... Qed. Lemma sv_subform_size : forall A B, sv_subform A B -> fsize A < fsize B . Proof. intros A B Hs. induction Hs ; simpl ; omega. Qed. Lemma sv_subform_antirefl : forall A, not (sv_subform A A) . Proof. intros A Hsv. apply sv_subform_size in Hsv. omega. 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 apply IHHs ; try assumption. intros B C Hs. induction Hs ; intros A0 Hs0... - apply sw_sub_vee_l... - apply sw_sub_vee_r... - apply sw_sub_wedge_l... - apply sw_sub_wedge_r... Qed. Definition w_subform A B := sw_subform A B \/ A = B. Inductive ww_subform : formula -> formula -> Prop := | ww_sub_id : forall A, ww_subform A A | ww_sub_wedge_l : forall A B C, ww_subform A B -> ww_subform A (wedge B C) | ww_sub_wedge_r : forall A B C, ww_subform A B -> ww_subform A (wedge C B) . Lemma ww_subform_trans : forall B C, ww_subform B C -> forall A, ww_subform A B -> ww_subform A C . Proof with try apply IHHs ; try assumption. intros B C Hs. induction Hs ; intros A0 Hs0... - apply ww_sub_wedge_l... - apply ww_sub_wedge_r... Qed. Lemma ww_w_subform : forall A B, ww_subform A B -> w_subform A B . Proof with assumption. intros A B Hww. induction Hww. - right ; reflexivity. - inversion IHHww. + left ; apply sw_sub_wedge_l... + subst ; left ; apply sw_sub_wedge_l_id. - inversion IHHww. + left ; apply sw_sub_wedge_r... + subst ; left ; apply sw_sub_wedge_r_id. Qed. Definition subformseq t A B R := (subform A R /\ subform B R) /\ (t = rr -> ww_subform A R) /\ (t = rr -> B = R) /\ ((t = rv \/ t = fc) -> sync A -> w_subform A R) /\ (t = rv -> sync B -> w_subform B R) /\ (t = fc -> async B -> sv_subform B R) /\ (t = rv -> B = R -> ww_subform A R) . Ltac subformseq_decomp := unfold subformseq ; (split ; [split | split ; [ | split ; [ | split ; [ | split ; [ | split]]]]]) ; try (intro Ht ; inversion Ht ; fail) ; try assumption ; try intro Ht . Ltac subformseq_simpl H := inversion H as [[Pss1 Pss2] [Pss3 [Pss4 [Pss5 [Pss6 [Pss7 Pss8]]]]]] ; subformseq_decomp . Notation "l ⊦⊦ ⇑ A , B" := (@polf (fun t' A' B' => subformseq t' A' B' A) max rr A B l) (at level 50). 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 (constructor ; fail). intros fs R t A B l pi. induction pi ; try (constructor ; try (constructor ; fail) ; apply IHpi ; fail). - 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, @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 (constructor ; fail). intros fs R t A B l pi. induction pi ; intro Pss ; try (constructor ; eassumption). - 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. left. eapply sw_subform_trans... * intro HA. apply subform_size in Pss2. simpl in Pss2. subst ; omega. + apply IHpi2. subformseq_simpl Pss. * eapply subform_trans... apply sub_wedge_r... * intro Hs. left. eapply sw_subform_trans... * intro HA. apply subform_size in Pss2. simpl in Pss2. subst ; omega. - apply wedge_rr_polf... + apply IHpi1. subformseq_simpl Pss. * eapply subform_trans ; [idtac | apply sub_wedge_l]... * eapply ww_subform_trans ; [idtac | apply ww_sub_wedge_l]... apply Pss3... * destruct Ht as [Ht | Ht] ; inversion Ht. + apply IHpi2. subformseq_simpl Pss. * eapply subform_trans ; [idtac | apply sub_wedge_r]... * eapply ww_subform_trans ; [idtac | apply ww_sub_wedge_r]... apply Pss3... * destruct Ht as [Ht | Ht] ; inversion Ht. - apply unfoc_fc_polf... apply IHpi. subformseq_simpl Pss. + apply Pss5. right... + intro Hs. inversion H0 ; subst ; inversion Hs. + intro HA. subst. apply Pss7 in H0... apply sv_subform_antirefl in H0. destruct H0. - apply unrev_rr_polf... apply IHpi. subformseq_simpl Pss. + intro Hs. apply ww_w_subform... apply Pss3... + intro Hs. assert (rr = rr) as He by reflexivity. apply Pss4 in He ; subst. right... + intro Hs. apply Pss3... - apply foc_l_rv_polf... apply IHpi. subformseq_simpl Pss. + apply Pss6... + intro Ha. inversion Ha ; inversion H0 ; subst ; inversion H2. - apply foc_r_rv_polf... apply IHpi. subformseq_simpl Pss. + apply Pss5. left... + intro Ha. inversion Ha ; inversion H0 ; subst ; inversion H2. - apply cw_rr_polf... apply IHpi. subformseq_simpl Pss. + intros _. apply ww_w_subform... apply Pss3... + intro Ha. inversion Ha. - apply cw_rv_polf... apply IHpi. subformseq_simpl Pss. + intros _. apply Pss6... + intro Ha. inversion Ha. Qed. (* Proposition 25 *) Proposition strong_sub_formula_diag : forall A l, l ⊦⊦ ⇑ A , A <-> l ⊦ ⇑ A , A . Proof with try reflexivity ; try eassumption. intros A l. split. - apply forget_strong_sub_formula. - intro pi. eapply strong_sub_formula in pi... subformseq_decomp ; try apply sub_id ; try apply ww_sub_id... intros. right... Qed. (* Automatic Backward Proof Search Tactic *) Ltac oauto := intros ; (try apply ax_fc_olf) || (try (apply vee_l_fc_olf ; oauto ; fail)) || (try (apply vee_r_fc_olf ; oauto ; fail)) || (try (apply top_rv_olf ; try auto_sync_async ; fail)) || (try apply top_rr_olf) || (try (apply wedge_rv_olf ; oauto ; fail)) || (try (apply wedge_rr_olf ; oauto ; fail)) || (try (apply unfoc_fc_olf ; [try auto_sync_async ; fail | oauto ; fail])) || (try (apply unrev_rr_olf ; oauto ; fail)) || (try (apply foc_l_rv_olf ; [try auto_sync_async ; fail | oauto ; fail])) || (try (apply foc_r_rv_olf ; [try auto_sync_async ; fail | oauto ; fail])) || (try (apply cw_rr_olf ; oauto ; fail)) || (try (apply cw_rv_olf ; [try auto_sync_async ; fail | oauto ; fail])) . (* Example 20 *) Example example2_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.