diff --git a/.gitignore b/.gitignore index 6eeea7e..b98fce2 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,6 @@ *.vo *.glob *.v.d +*.aux .depend +CONFIGURE diff --git a/Makefile b/Makefile index 1548a06..f95943b 100644 --- a/Makefile +++ b/Makefile @@ -1,11 +1,15 @@ CURRENT_DIR=./ -COQC=coqc -COQDEP=coqdep -slash +COQBIN= + +-include CONFIGURE + +COQC=$(COQBIN)coqc +COQDEP=$(COQBIN)coqdep DIRS = lib MinimunLogic PropositionalLogic SeparationLogic -INCLUDE_DEMO = $(foreach d, $(DIRS), -R $(CURRENT_DIR)/$(d) -as Logic.$(d)) +INCLUDE_DEMO = $(foreach d, $(DIRS), -R $(CURRENT_DIR)/$(d) Logic.$(d)) COQ_FLAG = $(INCLUDE_DEMO) -DEP_DEMO = -R $(CURRENT_DIR) -as Logic +DEP_DEMO = -R $(CURRENT_DIR) Logic DEP_FLAG = $(DEP_DEMO) lib_FILES = \ @@ -50,7 +54,7 @@ depend: @$(COQDEP) $(DEP_FLAG) $(FILES) > .depend clean: - @rm *.vo */*.vo *.glob */*.glob + @rm */*.vo */*.glob .DEFAULT_GOAL := all diff --git a/PropositionalLogic/Complete_Kripke.v b/PropositionalLogic/Complete_Kripke.v index 90276eb..8bcad14 100644 --- a/PropositionalLogic/Complete_Kripke.v +++ b/PropositionalLogic/Complete_Kripke.v @@ -1,570 +1,570 @@ -Require Import Coq.Logic.FunctionalExtensionality. -Require Import Coq.Logic.Classical_Prop. -Require Import Coq.Logic.Classical_Pred_Type. -Require Import Logic.lib.Bijection. -Require Import Logic.lib.Countable. -Require Import Logic.MinimunLogic.LogicBase. -Require Import Logic.MinimunLogic.MinimunLogic. -Require Import Logic.MinimunLogic.ContextProperty. -Require Import Logic.MinimunLogic.HenkinCompleteness. -Require Import Logic.PropositionalLogic.Syntax. -Require Import Logic.PropositionalLogic.IntuitionisticPropositionalLogic. -Require Import Logic.PropositionalLogic.GodelDummettLogic. -Require Import Logic.PropositionalLogic.ClassicalPropositionalLogic. -Require Import Logic.PropositionalLogic.KripkeSemantics. - -Local Open Scope logic_base. -Local Open Scope PropositionalLogic. - -Section GeneralCanonical. - -Context (Var: Type). -Context (CV: Countable Var). - -Instance L: Language := PropositionalLanguage.L Var. -Instance nL: NormalLanguage L := PropositionalLanguage.nL Var. -Instance pL: PropositionalLanguage L := PropositionalLanguage.pL Var. - -Definition DCS (Gamma: ProofTheory L): Type := sig (fun Phi => - derivable_closed Phi /\ - orp_witnessed Phi /\ - consistent Phi). - -Lemma DCS_ext {Gamma: ProofTheory L}: forall m n: DCS Gamma, - m = n <-> (forall x: expr, proj1_sig m x <-> proj1_sig n x). -Proof. - intros. - split; [intros; subst; reflexivity |]. - intros. - destruct m as [m ?H], n as [n ?H]. - simpl in H. - assert (m = n). - + apply Extensionality_Ensembles. - split; unfold Included, Ensembles.In; intros; apply H; auto. - + subst n. - assert (H0 = H1) by apply proof_irrelevance. - subst H1; auto. -Qed. - -Record canonical (Gamma: ProofTheory L) {SM: Semantics L} {pkSM: PreKripkeSemantics L SM} {kiSM: KripkeIntuitionisticSemantics L SM} (M: Kmodel): Type := { - underlying_surj :> surjection (Kworlds M) (DCS Gamma); - canonical_relation_sound: forall m n m' n', - underlying_surj m m' -> - underlying_surj n n' -> - Korder m n -> - Included _ (proj1_sig n') (proj1_sig m'); - canonical_relation_complete: forall n m' n', - underlying_surj n n' -> - Included _ (proj1_sig n') (proj1_sig m') -> - exists m, - underlying_surj m m' /\ Korder m n -}. - -Lemma Lindenbaum_lemma {Gamma: ProofTheory L} {nGamma: NormalProofTheory L Gamma} {mpGamma: MinimunPropositionalLogic L Gamma} {ipGamma: IntuitionisticPropositionalLogic L Gamma}: - forall Phi x, - ~ Phi |-- x -> - exists Psi, - Included _ Phi Psi /\ - ~ Psi |-- x /\ - derivable_closed Psi /\ - orp_witnessed Psi /\ - consistent Psi. -Proof. - intros. - assert (Countable expr) by (apply PropositionalLanguage.formula_countable; auto). - set (step := - fun n Phi x0 => - Phi x0 \/ - (X x0 n /\ - ~ (Union _ Phi (Singleton _ x0)) |-- x)). - exists (LindenbaumConstruction step Phi). - assert (Included expr Phi (LindenbaumConstruction step Phi) /\ - ~ LindenbaumConstruction step Phi |-- x /\ - (~ LindenbaumConstruction step Phi |-- x -> - derivable_closed (LindenbaumConstruction step Phi)) /\ - (~ LindenbaumConstruction step Phi |-- x -> - orp_witnessed (LindenbaumConstruction step Phi))). - Focus 2. { - destruct H0 as [? [? [? ?]]]. - split; [| split; [| split; [| split]]]; auto. - rewrite consistent_spec. - intro; apply H1. - pose proof deduction_falsep_elim _ x H4. - auto. - } Unfocus. - split; [| split; [| split]]. - + apply (Lindenbaum_spec_included _ _ 0). - + apply (Lindenbaum_spec_pos _ _ - (fun xs => |-- multi_imp xs x) - (fun Phi => Phi |-- x)). - - intros; apply derivable_provable. - - intros ? ? ? ?; left; auto. - - apply H. - - intros. - destruct (Classical_Prop.classic (exists x0, X x0 n /\ ~ (Union _ S (Singleton _ x0)) |-- x)) as [[x0 [? ?]] |]. - * intro; apply H2; clear H2. - eapply deduction_weaken; [| exact H3]. - hnf; intros ? [? | [? ?]]; [left; auto |]. - pose proof in_inj _ _ X _ _ _ H1 H2. - subst; right; constructor. - * intro; apply H0; clear H0. - eapply deduction_weaken; [| exact H2]. - hnf; intros ? [? | [? ?]]; [auto |]. - exfalso; apply H1; clear H1. - exists x0; auto. - + intros; hnf; intros. - destruct (im_inj _ _ X x0) as [n ?]. - apply (Lindenbaum_spec_neg _ _ _ (S n)). - simpl. - unfold step at 1. - right; split; auto. - intro. - rewrite deduction_theorem in H3. - eapply deduction_weaken in H3; [| apply (Lindenbaum_spec_included _ _ n)]. - pose proof deduction_modus_ponens _ _ _ H1 H3. - auto. - + intros; hnf; intros x0 y0 ?. - destruct (im_inj _ _ X x0) as [nx ?]. - destruct (im_inj _ _ X y0) as [ny ?]. - assert (LindenbaumChain step Phi (S nx) x0 \/ LindenbaumChain step Phi (S ny) y0) as HH; - [| destruct HH as [HH | HH]; apply Lindenbaum_spec_neg in HH; auto]. - simpl. - unfold step at 1 3. - assert (~ Union _ (LindenbaumChain step Phi nx) (Singleton _ x0) |-- x \/ - ~ Union _ (LindenbaumChain step Phi ny) (Singleton _ y0) |-- x) as HH; - [| destruct HH as [HH | HH]; auto]. - apply Classical_Prop.not_and_or; intros [? ?]. - rewrite deduction_theorem in H4, H5. - eapply deduction_weaken in H4; [| apply (Lindenbaum_spec_included _ _ nx)]. - eapply deduction_weaken in H5; [| apply (Lindenbaum_spec_included _ _ ny)]. - pose proof deduction_orp_elim (LindenbaumConstruction step Phi) x0 y0 x H4 H5. - apply (derivable_assum _ (x0 || y0)) in H1. - pose proof deduction_modus_ponens _ _ _ H1 H6. - auto. -Qed. - -Lemma truth_lemma {Gamma: ProofTheory L} {nGamma: NormalProofTheory L Gamma} {mpGamma: MinimunPropositionalLogic L Gamma} {ipGamma: IntuitionisticPropositionalLogic L Gamma} {SM: Semantics L} {pkSM: PreKripkeSemantics L SM} {kiSM: KripkeIntuitionisticSemantics L SM}: - forall M (X: canonical Gamma M), - (forall m Phi v, - X m Phi -> - (KRIPKE: M, m |= PropositionalLanguage.varp v <-> proj1_sig Phi (PropositionalLanguage.varp v))) -> - (forall m Phi, - X m Phi -> - forall x, KRIPKE: M, m |= x <-> proj1_sig Phi x). -Proof. - intros. - rename H into ATOM_ASSUM, H0 into H. - pose proof (fun Phi: DCS Gamma => derivable_closed_element_derivable (proj1_sig Phi) (proj1 (proj2_sig Phi))). - revert Phi m H. - induction x; try solve [inversion H1]; intros. - + specialize (IHx1 Phi m H). - specialize (IHx2 Phi m H). - pose proof DCS_andp_iff (proj1_sig Phi) (proj1 (proj2_sig Phi)) x1 x2. - change (PropositionalLanguage.andp x1 x2) with (x1 && x2). - rewrite sat_andp. - tauto. - + specialize (IHx1 Phi m H). - specialize (IHx2 Phi m H). - pose proof DCS_orp_iff (proj1_sig Phi) (proj1 (proj2_sig Phi)) (proj1 (proj2 (proj2_sig Phi))) x1 x2. - simpl in *. - change (PropositionalLanguage.orp x1 x2) with (x1 || x2). - rewrite sat_orp. - tauto. - + split. - - intros. - rewrite H0. - change (PropositionalLanguage.impp x1 x2) with (x1 --> x2) in *. - apply deduction_theorem. - apply Classical_Prop.NNPP; intro. - pose proof Lindenbaum_lemma _ _ H2. - destruct H3 as [Psi' [? [? ?]]]. - set (Psi := exist _ Psi' H5: DCS Gamma). - change Psi' with (proj1_sig Psi) in H3, H4. - clearbody Psi; clear Psi' H5. - rewrite sat_impp in H1. - assert (Included _ (proj1_sig Phi) (proj1_sig Psi)) by (hnf; intros; apply H3; left; auto). - destruct (canonical_relation_complete _ _ X m Psi Phi H H5) as [n [? ?]]. - specialize (H1 n H7). - rewrite IHx1, IHx2 in H1 by eauto. - assert (proj1_sig Psi x1) by (apply H3; right; constructor). - specialize (H1 H8). - specialize (H0 Psi x2). - rewrite H0 in H1; auto. - - intros. - change (PropositionalLanguage.impp x1 x2) with (x1 --> x2) in *. - rewrite sat_impp; intros n ?H. - destruct (im_surj _ _ X n) as [Psi ?]. - rewrite IHx1, IHx2 by eauto. - intros. - rewrite H0 in H1, H4 |- *. - eapply canonical_relation_sound in H2; [| eauto | eauto]. - eapply deduction_weaken in H1; [| exact H2]. - eapply deduction_modus_ponens; [exact H4 | exact H1]. - + pose proof sat_falsep M m. - split; [intros; tauto | intros]. - rewrite H0 in H2. - pose proof proj2_sig Phi. - destruct H3 as [_ [_ ?]]. - rewrite consistent_spec in H3. - exfalso; apply H3; auto. - + auto. -Qed. - -End GeneralCanonical. - -Module Canonical_All. - -Section Canonical_All. - -Context (Var: Type). -Context (CV: Countable Var). - -Instance L: Language := PropositionalLanguage.L Var. -Instance nL: NormalLanguage L := PropositionalLanguage.nL Var. -Instance pL: PropositionalLanguage L := PropositionalLanguage.pL Var. -Instance G: ProofTheory L := IntuitionisticPropositionalLogic.G Var. -Instance nG: NormalProofTheory L G := IntuitionisticPropositionalLogic.nG Var. -Instance mpG: MinimunPropositionalLogic L G := IntuitionisticPropositionalLogic.mpG Var. -Instance ipG: IntuitionisticPropositionalLogic L G := IntuitionisticPropositionalLogic.ipG Var. -Instance SM: Semantics L := KripkeSemantics_All.SM Var. -Instance pkSM: PreKripkeSemantics L SM := KripkeSemantics_All.pkSM Var. -Instance kiSM: KripkeIntuitionisticSemantics L SM := KripkeSemantics_All.kiSM Var. - -Definition canonical_frame: KripkeSemantics.frame. - refine (KripkeSemantics.Build_frame (DCS Var G) (fun a b => Included _ (proj1_sig b) (proj1_sig a)) _). - constructor. - + hnf; intros. - hnf; intros; auto. - + hnf; intros. - hnf; intros; auto. -Defined. - -Program Definition canonical_eval: Var -> KripkeSemantics.sem canonical_frame := - fun p a => a (PropositionalLanguage.varp p). -Next Obligation. - apply H; auto. -Qed. - -Definition canonical_Kmodel: KripkeSemantics_All.Kmodel := - KripkeSemantics_All.Build_Kmodel Var canonical_frame canonical_eval. - -Definition canonical_model (Phi: DCS Var G): model := - KripkeSemantics_All.Build_model Var canonical_Kmodel Phi. - -Definition canonical_Kmodel_surjection: surjection (KripkeSemantics.underlying_set (KripkeSemantics_All.underlying_frame canonical_Kmodel)) (DCS Var G). -Proof. - apply (FBuild_surjection _ _ id). - hnf; intros. - exists b; auto. -Defined. - -Lemma canonical_model_canonical: canonical Var G canonical_Kmodel. -Proof. - intros. - apply (Build_canonical _ _ _ _ _ _ canonical_Kmodel_surjection). - + intros. - change (DCS Var G) in m, n. - change (m = m') in H. - change (n = n') in H0. - subst n' m'. - auto. - + intros. - change (DCS Var G) in n, m'. - change (n = n') in H. - subst n. - exists m'. - split; auto. - change (m' = m'). - auto. -Defined. - -Lemma truth_lemma: forall (Phi: DCS Var G) x, canonical_model Phi |= x <-> proj1_sig Phi x. -Proof. - intros. - apply (truth_lemma Var CV _ canonical_model_canonical). - + intros. - hnf in H; unfold id in H; subst Phi0. - reflexivity. - + reflexivity. -Qed. - -Theorem complete_intuitionistic_kripke: strongly_complete G SM. -Proof. - assert (forall Phi x, ~ Phi |-- x -> ~ Phi |== x). - + intros. - assert (exists Psi: DCS Var G, Included _ Phi (proj1_sig Psi) /\ ~ proj1_sig Psi |-- x). - Focus 1. { - apply (Lindenbaum_lemma Var CV) in H. - destruct H as [Psi [? [? ?]]]. - exists (exist _ Psi H1). - simpl; auto. - } Unfocus. - destruct H0 as [Psi [? ?]]. - intro. - specialize (H2 (canonical_model Psi)). - apply H1. - rewrite <- derivable_closed_element_derivable by (exact (proj1 (proj2_sig Psi))). - rewrite <- truth_lemma. - apply H2; intros. - apply truth_lemma. - apply H0; auto. - + hnf; intros. - apply Classical_Prop.NNPP; intro; revert H0. - apply H; auto. -Qed. - -End Canonical_All. - -End Canonical_All. - -Module Canonical_Identical. - -Section Canonical_Identical. - -Context (Var: Type). -Context (CV: Countable Var). - -Instance L: Language := PropositionalLanguage.L Var. -Instance nL: NormalLanguage L := PropositionalLanguage.nL Var. -Instance pL: PropositionalLanguage L := PropositionalLanguage.pL Var. -Instance G: ProofTheory L := ClassicalPropositionalLogic.G Var. -Instance nG: NormalProofTheory L G := ClassicalPropositionalLogic.nG Var. -Instance mpG: MinimunPropositionalLogic L G := ClassicalPropositionalLogic.mpG Var. -Instance ipG: IntuitionisticPropositionalLogic L G := ClassicalPropositionalLogic.ipG Var. -Instance cpG: ClassicalPropositionalLogic L G := ClassicalPropositionalLogic.cpG Var. -Instance SM: Semantics L := KripkeSemantics_Identical.SM Var. -Instance pkSM: PreKripkeSemantics L SM := KripkeSemantics_Identical.pkSM Var. -Instance kiSM: KripkeIntuitionisticSemantics L SM := KripkeSemantics_Identical.kiSM Var. - -Definition canonical_frame: KripkeSemantics.frame. - refine (KripkeSemantics.Build_frame (DCS Var G) (fun a b => Included _ (proj1_sig b) (proj1_sig a)) _). - constructor. - + hnf; intros. - hnf; intros; auto. - + hnf; intros. - hnf; intros; auto. -Defined. - -Program Definition canonical_eval: Var -> KripkeSemantics.sem canonical_frame := - fun p a => a (PropositionalLanguage.varp p). -Next Obligation. - apply H; auto. -Qed. - -Program Definition canonical_Kmodel: @KripkeSemantics_Identical.Kmodel Var := - KripkeSemantics_Identical.Build_Kmodel Var canonical_frame canonical_eval _. -Next Obligation. - apply DCS_ext. - intros. - split; auto; [| apply H]. - intros. - rewrite DCS_negp_iff in H0 by (destruct (proj2_sig m); tauto). - assert (~ proj1_sig n (~~ x)) by (intro; apply H0, H; auto). - rewrite DCS_negp_iff by (destruct (proj2_sig n); tauto). - auto. -Qed. - -Definition canonical_model (Phi: DCS Var G): model := - KripkeSemantics_Identical.Build_model Var canonical_Kmodel Phi. - -Definition canonical_Kmodel_surjection: surjection (KripkeSemantics.underlying_set (KripkeSemantics_Identical.underlying_frame canonical_Kmodel)) (DCS Var G). -Proof. - apply (FBuild_surjection _ _ id). - hnf; intros. - exists b; auto. -Defined. - -Lemma canonical_model_canonical: canonical Var G canonical_Kmodel. -Proof. - intros. - apply (Build_canonical _ _ _ _ _ _ canonical_Kmodel_surjection). - + intros. - change (DCS Var G) in m, n. - change (m = m') in H. - change (n = n') in H0. - subst n' m'. - auto. - + intros. - change (DCS Var G) in n, m'. - change (n = n') in H. - subst n. - exists m'. - split; auto. - change (m' = m'). - auto. -Defined. - -Lemma truth_lemma: forall (Phi: DCS Var G) x, canonical_model Phi |= x <-> proj1_sig Phi x. -Proof. - intros. - apply (truth_lemma Var CV _ canonical_model_canonical). - + intros. - hnf in H; unfold id in H; subst Phi0. - reflexivity. - + reflexivity. -Qed. - -Theorem complete_intuitionistic_kripke: strongly_complete G SM. -Proof. - assert (forall Phi x, ~ Phi |-- x -> ~ Phi |== x). - + intros. - assert (exists Psi: DCS Var G, Included _ Phi (proj1_sig Psi) /\ ~ proj1_sig Psi |-- x). - Focus 1. { - apply (Lindenbaum_lemma Var CV) in H. - destruct H as [Psi [? [? ?]]]. - exists (exist _ Psi H1). - simpl; auto. - } Unfocus. - destruct H0 as [Psi [? ?]]. - intro. - specialize (H2 (canonical_model Psi)). - apply H1. - rewrite <- derivable_closed_element_derivable by (exact (proj1 (proj2_sig Psi))). - rewrite <- truth_lemma. - apply H2; intros. - apply truth_lemma. - apply H0; auto. - + hnf; intros. - apply Classical_Prop.NNPP; intro; revert H0. - apply H; auto. -Qed. - -End Canonical_Identical. - -End Canonical_Identical. - -Module Canonical_NoBranch. - -Section Canonical_NoBranch. - -Context (Var: Type). -Context (CV: Countable Var). - -Instance L: Language := PropositionalLanguage.L Var. -Instance nL: NormalLanguage L := PropositionalLanguage.nL Var. -Instance pL: PropositionalLanguage L := PropositionalLanguage.pL Var. -Instance G: ProofTheory L := GodelDummettPropositionalLogic.G Var. -Instance nG: NormalProofTheory L G := GodelDummettPropositionalLogic.nG Var. -Instance mpG: MinimunPropositionalLogic L G := GodelDummettPropositionalLogic.mpG Var. -Instance ipG: IntuitionisticPropositionalLogic L G := GodelDummettPropositionalLogic.ipG Var. -Instance wpG: GodelDummettPropositionalLogic L G := GodelDummettPropositionalLogic.wpG Var. -Instance SM: Semantics L := KripkeSemantics_NoBranch.SM Var. -Instance pkSM: PreKripkeSemantics L SM := KripkeSemantics_NoBranch.pkSM Var. -Instance kiSM: KripkeIntuitionisticSemantics L SM := KripkeSemantics_NoBranch.kiSM Var. - -Definition canonical_frame: KripkeSemantics.frame. - refine (KripkeSemantics.Build_frame (DCS Var G) (fun a b => Included _ (proj1_sig b) (proj1_sig a)) _). - constructor. - + hnf; intros. - hnf; intros; auto. - + hnf; intros. - hnf; intros; auto. -Defined. - -Program Definition canonical_eval: Var -> KripkeSemantics.sem canonical_frame := - fun p a => a (PropositionalLanguage.varp p). -Next Obligation. - apply H; auto. -Qed. - -Program Definition canonical_Kmodel: @KripkeSemantics_NoBranch.Kmodel Var := - KripkeSemantics_NoBranch.Build_Kmodel Var canonical_frame canonical_eval _. -Next Obligation. - destruct (classic (Included _ (proj1_sig m2) (proj1_sig m1))); auto. - destruct (classic (Included _ (proj1_sig m1) (proj1_sig m2))); auto. - exfalso. - unfold Included, Ensembles.In in H, H0, H1, H2. - apply not_all_ex_not in H1. - apply not_all_ex_not in H2. - destruct H1 as [x1 ?], H2 as [x2 ?]. - pose proof derivable_impp_choice (proj1_sig n) x1 x2. - rewrite <- derivable_closed_element_derivable in H3 by (destruct (proj2_sig n); tauto). - pose proof (proj1 (proj2 (proj2_sig n))). - apply H4 in H3; clear H4. - destruct H3; pose proof H3; apply H in H3; apply H0 in H4. - + rewrite derivable_closed_element_derivable in H3 by (destruct (proj2_sig m1); tauto). - rewrite derivable_closed_element_derivable in H4 by (destruct (proj2_sig m2); tauto). - pose proof (fun HH => deduction_modus_ponens _ _ _ HH H3). - pose proof (fun HH => deduction_modus_ponens _ _ _ HH H4). - rewrite <- !derivable_closed_element_derivable in H5 by (destruct (proj2_sig m1); tauto). - rewrite <- !derivable_closed_element_derivable in H6 by (destruct (proj2_sig m2); tauto). - clear - H1 H2 H5 H6. - tauto. - + rewrite derivable_closed_element_derivable in H3 by (destruct (proj2_sig m1); tauto). - rewrite derivable_closed_element_derivable in H4 by (destruct (proj2_sig m2); tauto). - pose proof (fun HH => deduction_modus_ponens _ _ _ HH H3). - pose proof (fun HH => deduction_modus_ponens _ _ _ HH H4). - rewrite <- !derivable_closed_element_derivable in H5 by (destruct (proj2_sig m1); tauto). - rewrite <- !derivable_closed_element_derivable in H6 by (destruct (proj2_sig m2); tauto). - clear - H1 H2 H5 H6. - tauto. -Qed. - -Definition canonical_model (Phi: DCS Var G): model := - KripkeSemantics_NoBranch.Build_model Var canonical_Kmodel Phi. - -Definition canonical_Kmodel_surjection: surjection (KripkeSemantics.underlying_set (KripkeSemantics_NoBranch.underlying_frame canonical_Kmodel)) (DCS Var G). -Proof. - apply (FBuild_surjection _ _ id). - hnf; intros. - exists b; auto. -Defined. - -Lemma canonical_model_canonical: canonical Var G canonical_Kmodel. -Proof. - intros. - apply (Build_canonical _ _ _ _ _ _ canonical_Kmodel_surjection). - + intros. - change (DCS Var G) in m, n. - change (m = m') in H. - change (n = n') in H0. - subst n' m'. - auto. - + intros. - change (DCS Var G) in n, m'. - change (n = n') in H. - subst n. - exists m'. - split; auto. - change (m' = m'). - auto. -Defined. - -Lemma truth_lemma: forall (Phi: DCS Var G) x, canonical_model Phi |= x <-> proj1_sig Phi x. -Proof. - intros. - apply (truth_lemma Var CV _ canonical_model_canonical). - + intros. - hnf in H; unfold id in H; subst Phi0. - reflexivity. - + reflexivity. -Qed. - -Theorem complete_intuitionistic_kripke: strongly_complete G SM. -Proof. - assert (forall Phi x, ~ Phi |-- x -> ~ Phi |== x). - + intros. - assert (exists Psi: DCS Var G, Included _ Phi (proj1_sig Psi) /\ ~ proj1_sig Psi |-- x). - Focus 1. { - apply (Lindenbaum_lemma Var CV) in H. - destruct H as [Psi [? [? ?]]]. - exists (exist _ Psi H1). - simpl; auto. - } Unfocus. - destruct H0 as [Psi [? ?]]. - intro. - specialize (H2 (canonical_model Psi)). - apply H1. - rewrite <- derivable_closed_element_derivable by (exact (proj1 (proj2_sig Psi))). - rewrite <- truth_lemma. - apply H2; intros. - apply truth_lemma. - apply H0; auto. - + hnf; intros. - apply Classical_Prop.NNPP; intro; revert H0. - apply H; auto. -Qed. - -End Canonical_NoBranch. - -End Canonical_NoBranch. +Require Import Coq.Logic.FunctionalExtensionality. +Require Import Coq.Logic.Classical_Prop. +Require Import Coq.Logic.Classical_Pred_Type. +Require Import Logic.lib.Bijection. +Require Import Logic.lib.Countable. +Require Import Logic.MinimunLogic.LogicBase. +Require Import Logic.MinimunLogic.MinimunLogic. +Require Import Logic.MinimunLogic.ContextProperty. +Require Import Logic.MinimunLogic.HenkinCompleteness. +Require Import Logic.PropositionalLogic.Syntax. +Require Import Logic.PropositionalLogic.IntuitionisticPropositionalLogic. +Require Import Logic.PropositionalLogic.GodelDummettLogic. +Require Import Logic.PropositionalLogic.ClassicalPropositionalLogic. +Require Import Logic.PropositionalLogic.KripkeSemantics. + +Local Open Scope logic_base. +Local Open Scope PropositionalLogic. + +Section GeneralCanonical. + +Context (Var: Type). +Context (CV: Countable Var). + +Instance L: Language := PropositionalLanguage.L Var. +Instance nL: NormalLanguage L := PropositionalLanguage.nL Var. +Instance pL: PropositionalLanguage L := PropositionalLanguage.pL Var. + +Definition DCS (Gamma: ProofTheory L): Type := sig (fun Phi => + derivable_closed Phi /\ + orp_witnessed Phi /\ + consistent Phi). + +Lemma DCS_ext {Gamma: ProofTheory L}: forall m n: DCS Gamma, + m = n <-> (forall x: expr, proj1_sig m x <-> proj1_sig n x). +Proof. + intros. + split; [intros; subst; reflexivity |]. + intros. + destruct m as [m ?H], n as [n ?H]. + simpl in H. + assert (m = n). + + apply Extensionality_Ensembles. + split; unfold Included, Ensembles.In; intros; apply H; auto. + + subst n. + assert (H0 = H1) by apply proof_irrelevance. + subst H1; auto. +Qed. + +Record canonical (Gamma: ProofTheory L) {SM: Semantics L} {pkSM: PreKripkeSemantics L SM} {kiSM: KripkeIntuitionisticSemantics L SM} (M: Kmodel): Type := { + underlying_surj :> surjection (Kworlds M) (DCS Gamma); + canonical_relation_sound: forall m n m' n', + underlying_surj m m' -> + underlying_surj n n' -> + Korder m n -> + Included _ (proj1_sig n') (proj1_sig m'); + canonical_relation_complete: forall n m' n', + underlying_surj n n' -> + Included _ (proj1_sig n') (proj1_sig m') -> + exists m, + underlying_surj m m' /\ Korder m n +}. + +Lemma Lindenbaum_lemma {Gamma: ProofTheory L} {nGamma: NormalProofTheory L Gamma} {mpGamma: MinimunPropositionalLogic L Gamma} {ipGamma: IntuitionisticPropositionalLogic L Gamma}: + forall Phi x, + ~ Phi |-- x -> + exists Psi, + Included _ Phi Psi /\ + ~ Psi |-- x /\ + derivable_closed Psi /\ + orp_witnessed Psi /\ + consistent Psi. +Proof. + intros. + assert (Countable expr) by (apply PropositionalLanguage.formula_countable; auto). + set (step := + fun n Phi x0 => + Phi x0 \/ + (X x0 n /\ + ~ (Union _ Phi (Singleton _ x0)) |-- x)). + exists (LindenbaumConstruction step Phi). + assert (Included expr Phi (LindenbaumConstruction step Phi) /\ + ~ LindenbaumConstruction step Phi |-- x /\ + (~ LindenbaumConstruction step Phi |-- x -> + derivable_closed (LindenbaumConstruction step Phi)) /\ + (~ LindenbaumConstruction step Phi |-- x -> + orp_witnessed (LindenbaumConstruction step Phi))). + Focus 2. { + destruct H0 as [? [? [? ?]]]. + split; [| split; [| split; [| split]]]; auto. + rewrite consistent_spec. + intro; apply H1. + pose proof deduction_falsep_elim _ x H4. + auto. + } Unfocus. + split; [| split; [| split]]. + + apply (Lindenbaum_spec_included _ _ 0). + + apply (Lindenbaum_spec_pos _ _ + (fun xs => |-- multi_imp xs x) + (fun Phi => Phi |-- x)). + - intros; apply derivable_provable. + - intros ? ? ? ?; left; auto. + - apply H. + - intros. + destruct (Classical_Prop.classic (exists x0, X x0 n /\ ~ (Union _ S (Singleton _ x0)) |-- x)) as [[x0 [? ?]] |]. + * intro; apply H2; clear H2. + eapply deduction_weaken; [| exact H3]. + hnf; intros ? [? | [? ?]]; [left; auto |]. + pose proof in_inj _ _ X _ _ _ H1 H2. + subst; right; constructor. + * intro; apply H0; clear H0. + eapply deduction_weaken; [| exact H2]. + hnf; intros ? [? | [? ?]]; [auto |]. + exfalso; apply H1; clear H1. + exists x0; auto. + + intros; hnf; intros. + destruct (im_inj _ _ X x0) as [n ?]. + apply (Lindenbaum_spec_neg _ _ _ (S n)). + simpl. + unfold step at 1. + right; split; auto. + intro. + rewrite deduction_theorem in H3. + eapply deduction_weaken in H3; [| apply (Lindenbaum_spec_included _ _ n)]. + pose proof deduction_modus_ponens _ _ _ H1 H3. + auto. + + intros; hnf; intros x0 y0 ?. + destruct (im_inj _ _ X x0) as [nx ?]. + destruct (im_inj _ _ X y0) as [ny ?]. + assert (LindenbaumChain step Phi (S nx) x0 \/ LindenbaumChain step Phi (S ny) y0) as HH; + [| destruct HH as [HH | HH]; apply Lindenbaum_spec_neg in HH; auto]. + simpl. + unfold step at 1 3. + assert (~ Union _ (LindenbaumChain step Phi nx) (Singleton _ x0) |-- x \/ + ~ Union _ (LindenbaumChain step Phi ny) (Singleton _ y0) |-- x) as HH; + [| destruct HH as [HH | HH]; auto]. + apply Classical_Prop.not_and_or; intros [? ?]. + rewrite deduction_theorem in H4, H5. + eapply deduction_weaken in H4; [| apply (Lindenbaum_spec_included _ _ nx)]. + eapply deduction_weaken in H5; [| apply (Lindenbaum_spec_included _ _ ny)]. + pose proof deduction_orp_elim (LindenbaumConstruction step Phi) x0 y0 x H4 H5. + apply (derivable_assum _ (x0 || y0)) in H1. + pose proof deduction_modus_ponens _ _ _ H1 H6. + auto. +Qed. + +Lemma truth_lemma {Gamma: ProofTheory L} {nGamma: NormalProofTheory L Gamma} {mpGamma: MinimunPropositionalLogic L Gamma} {ipGamma: IntuitionisticPropositionalLogic L Gamma} {SM: Semantics L} {pkSM: PreKripkeSemantics L SM} {kiSM: KripkeIntuitionisticSemantics L SM}: + forall M (X: canonical Gamma M), + (forall m Phi v, + X m Phi -> + (KRIPKE: M, m |= PropositionalLanguage.varp v <-> proj1_sig Phi (PropositionalLanguage.varp v))) -> + (forall m Phi, + X m Phi -> + forall x, KRIPKE: M, m |= x <-> proj1_sig Phi x). +Proof. + intros. + rename H into ATOM_ASSUM, H0 into H. + pose proof (fun Phi: DCS Gamma => derivable_closed_element_derivable (proj1_sig Phi) (proj1 (proj2_sig Phi))). + revert Phi m H. + induction x; try solve [inversion H1]; intros. + + specialize (IHx1 Phi m H). + specialize (IHx2 Phi m H). + pose proof DCS_andp_iff (proj1_sig Phi) (proj1 (proj2_sig Phi)) x1 x2. + change (PropositionalLanguage.andp x1 x2) with (x1 && x2). + rewrite sat_andp. + tauto. + + specialize (IHx1 Phi m H). + specialize (IHx2 Phi m H). + pose proof DCS_orp_iff (proj1_sig Phi) (proj1 (proj2_sig Phi)) (proj1 (proj2 (proj2_sig Phi))) x1 x2. + simpl in *. + change (PropositionalLanguage.orp x1 x2) with (x1 || x2). + rewrite sat_orp. + tauto. + + split. + - intros. + rewrite H0. + change (PropositionalLanguage.impp x1 x2) with (x1 --> x2) in *. + apply deduction_theorem. + apply Classical_Prop.NNPP; intro. + pose proof Lindenbaum_lemma _ _ H2. + destruct H3 as [Psi' [? [? ?]]]. + set (Psi := exist _ Psi' H5: DCS Gamma). + change Psi' with (proj1_sig Psi) in H3, H4. + clearbody Psi; clear Psi' H5. + rewrite sat_impp in H1. + assert (Included _ (proj1_sig Phi) (proj1_sig Psi)) by (hnf; intros; apply H3; left; auto). + destruct (canonical_relation_complete _ _ X m Psi Phi H H5) as [n [? ?]]. + specialize (H1 n H7). + rewrite IHx1, IHx2 in H1 by eauto. + assert (proj1_sig Psi x1) by (apply H3; right; constructor). + specialize (H1 H8). + specialize (H0 Psi x2). + rewrite H0 in H1; auto. + - intros. + change (PropositionalLanguage.impp x1 x2) with (x1 --> x2) in *. + rewrite sat_impp; intros n ?H. + destruct (im_surj _ _ X n) as [Psi ?]. + rewrite IHx1, IHx2 by eauto. + intros. + rewrite H0 in H1, H4 |- *. + eapply canonical_relation_sound in H2; [| eauto | eauto]. + eapply deduction_weaken in H1; [| exact H2]. + eapply deduction_modus_ponens; [exact H4 | exact H1]. + + pose proof sat_falsep M m. + split; [intros; tauto | intros]. + rewrite H0 in H2. + pose proof proj2_sig Phi. + destruct H3 as [_ [_ ?]]. + rewrite consistent_spec in H3. + exfalso; apply H3; auto. + + auto. +Qed. + +End GeneralCanonical. + +Module Canonical_All. + +Section Canonical_All. + +Context (Var: Type). +Context (CV: Countable Var). + +Instance L: Language := PropositionalLanguage.L Var. +Instance nL: NormalLanguage L := PropositionalLanguage.nL Var. +Instance pL: PropositionalLanguage L := PropositionalLanguage.pL Var. +Instance G: ProofTheory L := IntuitionisticPropositionalLogic.G Var. +Instance nG: NormalProofTheory L G := IntuitionisticPropositionalLogic.nG Var. +Instance mpG: MinimunPropositionalLogic L G := IntuitionisticPropositionalLogic.mpG Var. +Instance ipG: IntuitionisticPropositionalLogic L G := IntuitionisticPropositionalLogic.ipG Var. +Instance SM: Semantics L := KripkeSemantics_All.SM Var. +Instance pkSM: PreKripkeSemantics L SM := KripkeSemantics_All.pkSM Var. +Instance kiSM: KripkeIntuitionisticSemantics L SM := KripkeSemantics_All.kiSM Var. + +Definition canonical_frame: KripkeSemantics.frame. + refine (KripkeSemantics.Build_frame (DCS Var G) (fun a b => Included _ (proj1_sig b) (proj1_sig a)) _). + constructor. + + hnf; intros. + hnf; intros; auto. + + hnf; intros. + hnf; intros; auto. +Defined. + +Program Definition canonical_eval: Var -> KripkeSemantics.sem canonical_frame := + fun p a => a (PropositionalLanguage.varp p). +Next Obligation. + apply H; auto. +Qed. + +Definition canonical_Kmodel: KripkeSemantics_All.Kmodel := + KripkeSemantics_All.Build_Kmodel Var canonical_frame canonical_eval. + +Definition canonical_model (Phi: DCS Var G): model := + KripkeSemantics_All.Build_model Var canonical_Kmodel Phi. + +Definition canonical_Kmodel_surjection: surjection (Kworlds canonical_Kmodel) (DCS Var G). +Proof. + apply (FBuild_surjection _ _ id). + hnf; intros. + exists b; auto. +Defined. + +Lemma canonical_model_canonical: canonical Var G canonical_Kmodel. +Proof. + intros. + apply (Build_canonical _ _ _ _ _ _ canonical_Kmodel_surjection). + + intros. + change (DCS Var G) in m, n. + change (m = m') in H. + change (n = n') in H0. + subst n' m'. + auto. + + intros. + change (DCS Var G) in n, m'. + change (n = n') in H. + subst n. + exists m'. + split; auto. + change (m' = m'). + auto. +Defined. + +Lemma truth_lemma: forall (Phi: DCS Var G) x, canonical_model Phi |= x <-> proj1_sig Phi x. +Proof. + intros. + apply (truth_lemma Var CV _ canonical_model_canonical). + + intros. + hnf in H; unfold id in H; subst Phi0. + reflexivity. + + reflexivity. +Qed. + +Theorem complete_intuitionistic_kripke: strongly_complete G SM. +Proof. + assert (forall Phi x, ~ Phi |-- x -> ~ Phi |== x). + + intros. + assert (exists Psi: DCS Var G, Included _ Phi (proj1_sig Psi) /\ ~ proj1_sig Psi |-- x). + Focus 1. { + apply (Lindenbaum_lemma Var CV) in H. + destruct H as [Psi [? [? ?]]]. + exists (exist _ Psi H1). + simpl; auto. + } Unfocus. + destruct H0 as [Psi [? ?]]. + intro. + specialize (H2 (canonical_model Psi)). + apply H1. + rewrite <- derivable_closed_element_derivable by (exact (proj1 (proj2_sig Psi))). + rewrite <- truth_lemma. + apply H2; intros. + apply truth_lemma. + apply H0; auto. + + hnf; intros. + apply Classical_Prop.NNPP; intro; revert H0. + apply H; auto. +Qed. + +End Canonical_All. + +End Canonical_All. + +Module Canonical_Identical. + +Section Canonical_Identical. + +Context (Var: Type). +Context (CV: Countable Var). + +Instance L: Language := PropositionalLanguage.L Var. +Instance nL: NormalLanguage L := PropositionalLanguage.nL Var. +Instance pL: PropositionalLanguage L := PropositionalLanguage.pL Var. +Instance G: ProofTheory L := ClassicalPropositionalLogic.G Var. +Instance nG: NormalProofTheory L G := ClassicalPropositionalLogic.nG Var. +Instance mpG: MinimunPropositionalLogic L G := ClassicalPropositionalLogic.mpG Var. +Instance ipG: IntuitionisticPropositionalLogic L G := ClassicalPropositionalLogic.ipG Var. +Instance cpG: ClassicalPropositionalLogic L G := ClassicalPropositionalLogic.cpG Var. +Instance SM: Semantics L := KripkeSemantics_Identical.SM Var. +Instance pkSM: PreKripkeSemantics L SM := KripkeSemantics_Identical.pkSM Var. +Instance kiSM: KripkeIntuitionisticSemantics L SM := KripkeSemantics_Identical.kiSM Var. + +Definition canonical_frame: KripkeSemantics.frame. + refine (KripkeSemantics.Build_frame (DCS Var G) (fun a b => Included _ (proj1_sig b) (proj1_sig a)) _). + constructor. + + hnf; intros. + hnf; intros; auto. + + hnf; intros. + hnf; intros; auto. +Defined. + +Program Definition canonical_eval: Var -> KripkeSemantics.sem canonical_frame := + fun p a => a (PropositionalLanguage.varp p). +Next Obligation. + apply H; auto. +Qed. + +Program Definition canonical_Kmodel: @KripkeSemantics_Identical.Kmodel Var := + KripkeSemantics_Identical.Build_Kmodel Var canonical_frame canonical_eval _. +Next Obligation. + apply DCS_ext. + intros. + split; auto; [| apply H]. + intros. + rewrite DCS_negp_iff in H0 by (destruct (proj2_sig m); tauto). + assert (~ proj1_sig n (~~ x)) by (intro; apply H0, H; auto). + rewrite DCS_negp_iff by (destruct (proj2_sig n); tauto). + auto. +Qed. + +Definition canonical_model (Phi: DCS Var G): model := + KripkeSemantics_Identical.Build_model Var canonical_Kmodel Phi. + +Definition canonical_Kmodel_surjection: surjection (Kworlds canonical_Kmodel) (DCS Var G). +Proof. + apply (FBuild_surjection _ _ id). + hnf; intros. + exists b; auto. +Defined. + +Lemma canonical_model_canonical: canonical Var G canonical_Kmodel. +Proof. + intros. + apply (Build_canonical _ _ _ _ _ _ canonical_Kmodel_surjection). + + intros. + change (DCS Var G) in m, n. + change (m = m') in H. + change (n = n') in H0. + subst n' m'. + auto. + + intros. + change (DCS Var G) in n, m'. + change (n = n') in H. + subst n. + exists m'. + split; auto. + change (m' = m'). + auto. +Defined. + +Lemma truth_lemma: forall (Phi: DCS Var G) x, canonical_model Phi |= x <-> proj1_sig Phi x. +Proof. + intros. + apply (truth_lemma Var CV _ canonical_model_canonical). + + intros. + hnf in H; unfold id in H; subst Phi0. + reflexivity. + + reflexivity. +Qed. + +Theorem complete_intuitionistic_kripke: strongly_complete G SM. +Proof. + assert (forall Phi x, ~ Phi |-- x -> ~ Phi |== x). + + intros. + assert (exists Psi: DCS Var G, Included _ Phi (proj1_sig Psi) /\ ~ proj1_sig Psi |-- x). + Focus 1. { + apply (Lindenbaum_lemma Var CV) in H. + destruct H as [Psi [? [? ?]]]. + exists (exist _ Psi H1). + simpl; auto. + } Unfocus. + destruct H0 as [Psi [? ?]]. + intro. + specialize (H2 (canonical_model Psi)). + apply H1. + rewrite <- derivable_closed_element_derivable by (exact (proj1 (proj2_sig Psi))). + rewrite <- truth_lemma. + apply H2; intros. + apply truth_lemma. + apply H0; auto. + + hnf; intros. + apply Classical_Prop.NNPP; intro; revert H0. + apply H; auto. +Qed. + +End Canonical_Identical. + +End Canonical_Identical. + +Module Canonical_NoBranch. + +Section Canonical_NoBranch. + +Context (Var: Type). +Context (CV: Countable Var). + +Instance L: Language := PropositionalLanguage.L Var. +Instance nL: NormalLanguage L := PropositionalLanguage.nL Var. +Instance pL: PropositionalLanguage L := PropositionalLanguage.pL Var. +Instance G: ProofTheory L := GodelDummettPropositionalLogic.G Var. +Instance nG: NormalProofTheory L G := GodelDummettPropositionalLogic.nG Var. +Instance mpG: MinimunPropositionalLogic L G := GodelDummettPropositionalLogic.mpG Var. +Instance ipG: IntuitionisticPropositionalLogic L G := GodelDummettPropositionalLogic.ipG Var. +Instance wpG: GodelDummettPropositionalLogic L G := GodelDummettPropositionalLogic.wpG Var. +Instance SM: Semantics L := KripkeSemantics_NoBranch.SM Var. +Instance pkSM: PreKripkeSemantics L SM := KripkeSemantics_NoBranch.pkSM Var. +Instance kiSM: KripkeIntuitionisticSemantics L SM := KripkeSemantics_NoBranch.kiSM Var. + +Definition canonical_frame: KripkeSemantics.frame. + refine (KripkeSemantics.Build_frame (DCS Var G) (fun a b => Included _ (proj1_sig b) (proj1_sig a)) _). + constructor. + + hnf; intros. + hnf; intros; auto. + + hnf; intros. + hnf; intros; auto. +Defined. + +Program Definition canonical_eval: Var -> KripkeSemantics.sem canonical_frame := + fun p a => a (PropositionalLanguage.varp p). +Next Obligation. + apply H; auto. +Qed. + +Program Definition canonical_Kmodel: @KripkeSemantics_NoBranch.Kmodel Var := + KripkeSemantics_NoBranch.Build_Kmodel Var canonical_frame canonical_eval _. +Next Obligation. + destruct (classic (Included _ (proj1_sig m2) (proj1_sig m1))); auto. + destruct (classic (Included _ (proj1_sig m1) (proj1_sig m2))); auto. + exfalso. + unfold Included, Ensembles.In in H, H0, H1, H2. + apply not_all_ex_not in H1. + apply not_all_ex_not in H2. + destruct H1 as [x1 ?], H2 as [x2 ?]. + pose proof derivable_impp_choice (proj1_sig n) x1 x2. + rewrite <- derivable_closed_element_derivable in H3 by (destruct (proj2_sig n); tauto). + pose proof (proj1 (proj2 (proj2_sig n))). + apply H4 in H3; clear H4. + destruct H3; pose proof H3; apply H in H3; apply H0 in H4. + + rewrite derivable_closed_element_derivable in H3 by (destruct (proj2_sig m1); tauto). + rewrite derivable_closed_element_derivable in H4 by (destruct (proj2_sig m2); tauto). + pose proof (fun HH => deduction_modus_ponens _ _ _ HH H3). + pose proof (fun HH => deduction_modus_ponens _ _ _ HH H4). + rewrite <- !derivable_closed_element_derivable in H5 by (destruct (proj2_sig m1); tauto). + rewrite <- !derivable_closed_element_derivable in H6 by (destruct (proj2_sig m2); tauto). + clear - H1 H2 H5 H6. + tauto. + + rewrite derivable_closed_element_derivable in H3 by (destruct (proj2_sig m1); tauto). + rewrite derivable_closed_element_derivable in H4 by (destruct (proj2_sig m2); tauto). + pose proof (fun HH => deduction_modus_ponens _ _ _ HH H3). + pose proof (fun HH => deduction_modus_ponens _ _ _ HH H4). + rewrite <- !derivable_closed_element_derivable in H5 by (destruct (proj2_sig m1); tauto). + rewrite <- !derivable_closed_element_derivable in H6 by (destruct (proj2_sig m2); tauto). + clear - H1 H2 H5 H6. + tauto. +Qed. + +Definition canonical_model (Phi: DCS Var G): model := + KripkeSemantics_NoBranch.Build_model Var canonical_Kmodel Phi. + +Definition canonical_Kmodel_surjection: surjection (Kworlds canonical_Kmodel) (DCS Var G). +Proof. + apply (FBuild_surjection _ _ id). + hnf; intros. + exists b; auto. +Defined. + +Lemma canonical_model_canonical: canonical Var G canonical_Kmodel. +Proof. + intros. + apply (Build_canonical _ _ _ _ _ _ canonical_Kmodel_surjection). + + intros. + change (DCS Var G) in m, n. + change (m = m') in H. + change (n = n') in H0. + subst n' m'. + auto. + + intros. + change (DCS Var G) in n, m'. + change (n = n') in H. + subst n. + exists m'. + split; auto. + change (m' = m'). + auto. +Defined. + +Lemma truth_lemma: forall (Phi: DCS Var G) x, canonical_model Phi |= x <-> proj1_sig Phi x. +Proof. + intros. + apply (truth_lemma Var CV _ canonical_model_canonical). + + intros. + hnf in H; unfold id in H; subst Phi0. + reflexivity. + + reflexivity. +Qed. + +Theorem complete_intuitionistic_kripke: strongly_complete G SM. +Proof. + assert (forall Phi x, ~ Phi |-- x -> ~ Phi |== x). + + intros. + assert (exists Psi: DCS Var G, Included _ Phi (proj1_sig Psi) /\ ~ proj1_sig Psi |-- x). + Focus 1. { + apply (Lindenbaum_lemma Var CV) in H. + destruct H as [Psi [? [? ?]]]. + exists (exist _ Psi H1). + simpl; auto. + } Unfocus. + destruct H0 as [Psi [? ?]]. + intro. + specialize (H2 (canonical_model Psi)). + apply H1. + rewrite <- derivable_closed_element_derivable by (exact (proj1 (proj2_sig Psi))). + rewrite <- truth_lemma. + apply H2; intros. + apply truth_lemma. + apply H0; auto. + + hnf; intros. + apply Classical_Prop.NNPP; intro; revert H0. + apply H; auto. +Qed. + +End Canonical_NoBranch. + +End Canonical_NoBranch. diff --git a/PropositionalLogic/Syntax.v b/PropositionalLogic/Syntax.v index dd826da..b9bf01b 100644 --- a/PropositionalLogic/Syntax.v +++ b/PropositionalLogic/Syntax.v @@ -1,123 +1,125 @@ -Require Import Coq.Logic.ProofIrrelevance. -Require Import Logic.lib.Bijection. -Require Import Logic.lib.Countable. -Require Import Logic.MinimunLogic.LogicBase. -Require Import Logic.MinimunLogic.MinimunLogic. - -Class PropositionalLanguage (L: Language) {nL: NormalLanguage L}: Type := { - andp : expr -> expr -> expr; - orp : expr -> expr -> expr; - falsep: expr -}. - -Definition negp {L: Language} {nL: NormalLanguage L} {pL: PropositionalLanguage L} (x: expr): expr := impp x falsep. -Definition iffp {L: Language} {nL: NormalLanguage L} {pL: PropositionalLanguage L} (x y: expr): expr := andp (impp x y) (impp y x). -Definition truep {L: Language} {nL: NormalLanguage L} {pL: PropositionalLanguage L}: expr := impp falsep falsep. - -Notation "x && y" := (andp x y) (at level 40, left associativity) : PropositionalLogic. -Notation "x || y" := (orp x y) (at level 50, left associativity) : PropositionalLogic. -Notation "x <--> y" := (iffp x y) (at level 60, no associativity) : PropositionalLogic. -Notation "~~ x" := (negp x) (at level 35) : PropositionalLogic. -Notation "'FF'" := falsep : PropositionalLogic. -Notation "'TT'" := truep : PropositionalLogic. - -Local Open Scope logic_base. -Local Open Scope PropositionalLogic. - -Definition orp_witnessed {L: Language} {nL: NormalLanguage L} {pL: PropositionalLanguage L} {Gamma: ProofTheory L}: context -> Prop := - fun Phi => forall x y, Phi (x || y) -> Phi x \/ Phi y. - -Module PropositionalLanguage. - -Inductive expr {Var: Type}: Type := - | andp : expr -> expr -> expr - | orp : expr -> expr -> expr - | impp : expr -> expr -> expr - | falsep : expr - | varp : Var -> expr. - -Implicit Arguments expr. - -Instance L (Var: Type): Language := - Build_Language (expr Var). - -Instance nL (Var: Type): NormalLanguage (L Var) := - Build_NormalLanguage (L Var) impp. - -Instance pL (Var: Type): PropositionalLanguage (L Var) := - Build_PropositionalLanguage (L Var) (nL Var) andp orp falsep. - -Definition rank {Var: Type}: expr Var -> nat := - fix rank (x: expr Var): nat := - match x with - | andp y z => 1 + rank y + rank z - | orp y z => 1 + rank y + rank z - | impp y z => 1 + rank y + rank z - | falsep => 0 - | varp p => 0 - end. - -Definition formula_countable: forall Var, Countable Var -> Countable (expr Var). - intros. - assert (forall n, Countable (sig (fun x: expr Var => rank x <= n))). - + induction n. - - apply (@bijection_Countable _ (Var + unit)%type); [| solve_Countable]. - apply bijection_sym. - apply (FBuild_bijection _ _ (fun x => - match x with - | inl p => exist (fun x: expr Var => rank x <= 0) (varp p) (le_n 0) - | inr _ => exist (fun x: expr Var => rank x <= 0) falsep (le_n 0) - end)). - * hnf; intros. - destruct a1 as [? | []], a2 as [? | []]; inversion H; auto. - * hnf; intros. - destruct b as [[] HH]; try solve [inversion HH]. - 1: exists (inr tt); eauto; f_equal; apply proof_irrelevance. - 1: exists (inl v); eauto; f_equal; apply proof_irrelevance. - - set (s := sig (fun x: expr Var => rank x <= n)). - apply (@injection_Countable _ (s * s + s * s + s * s + unit + Var)%type); [| solve_Countable]. - apply (Build_injection _ _ (fun x y => - match y with - | inl (inl (inl (inl (exist y _, exist z _)))) => proj1_sig x = andp y z - | inl (inl (inl (inr (exist y _, exist z _)))) => proj1_sig x = orp y z - | inl (inl (inr (exist y _, exist z _))) => proj1_sig x = impp y z - | inl (inr _) => proj1_sig x = falsep - | inr p => proj1_sig x = varp p - end)). - * hnf; intros. - destruct a as [[y z | y z | y z | | p] ?H]. - (* 1 *) simpl in H. assert (rank y <= n) by omega. assert (rank z <= n) by omega. - exists (inl (inl (inl (inl (exist _ y H0, exist _ z H1))))); auto. - (* 2 *) simpl in H. assert (rank y <= n) by omega. assert (rank z <= n) by omega. - exists (inl (inl (inl (inr (exist _ y H0, exist _ z H1))))); auto. - (* 3 *) simpl in H. assert (rank y <= n) by omega. assert (rank z <= n) by omega. - exists (inl (inl (inr (exist _ y H0, exist _ z H1)))); auto. - (* 4 *) exists (inl (inr tt)); auto. - (* 5 *) exists (inr p); auto. - * hnf; intros. - destruct a as [[y z | y z | y z | | p] ?H]; - destruct b1 as [[[[[[y1 ?H] [z1 ?H]] | [[y1 ?H] [z1 ?H]]] | [[y1 ?H] [z1 ?H]]] |] | p1]; try solve [inversion H]; - destruct b2 as [[[[[[y2 ?H] [z2 ?H]] | [[y2 ?H] [z2 ?H]]] | [[y2 ?H] [z2 ?H]]] |] | p2]; try solve [inversion H0]. - (* 1 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance. - (* 2 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance. - (* 3 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance. - (* 4 *) destruct u, u0; auto. - (* 5 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance. - * hnf; intros. - destruct b as [[[[[[y ?H] [z ?H]] | [[y ?H] [z ?H]]] | [[y ?H] [z ?H]]] |] | p]; - destruct a1 as [[y1 z1 | y1 z1 | y1 z1 | | p1] ?H]; try solve [inversion H]; - destruct a2 as [[y2 z2 | y2 z2 | y2 z2 | | p2] ?H]; try solve [inversion H0]. - (* 1 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance. - (* 2 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance. - (* 3 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance. - (* 4 *) f_equal; apply proof_irrelevance. - (* 5 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance. - + apply (@injection_Countable _ (sigT (fun n => sig (fun x: expr Var => rank x <= n)))); [| solve_Countable; auto]. - apply (FBuild_injection _ _ (fun x => existT _ (rank x) (exist _ x (le_n _)))). - hnf; intros. - simpl in H. - inversion H; auto. -Qed. (* 20 seconds *) - -End PropositionalLanguage. - +Require Import Coq.Logic.ProofIrrelevance. +Require Import Logic.lib.Bijection. +Require Import Logic.lib.Countable. +Require Import Logic.MinimunLogic.LogicBase. +Require Import Logic.MinimunLogic.MinimunLogic. +Require Import Omega. + +Class PropositionalLanguage (L: Language) {nL: NormalLanguage L}: Type := { + andp : expr -> expr -> expr; + orp : expr -> expr -> expr; + falsep: expr +}. + +Definition negp {L: Language} {nL: NormalLanguage L} {pL: PropositionalLanguage L} (x: expr): expr := impp x falsep. +Definition iffp {L: Language} {nL: NormalLanguage L} {pL: PropositionalLanguage L} (x y: expr): expr := andp (impp x y) (impp y x). +Definition truep {L: Language} {nL: NormalLanguage L} {pL: PropositionalLanguage L}: expr := impp falsep falsep. + +Notation "x && y" := (andp x y) (at level 40, left associativity) : PropositionalLogic. +Notation "x || y" := (orp x y) (at level 50, left associativity) : PropositionalLogic. +Notation "x <--> y" := (iffp x y) (at level 60, no associativity) : PropositionalLogic. +Notation "~~ x" := (negp x) (at level 35) : PropositionalLogic. +Notation "'FF'" := falsep : PropositionalLogic. +Notation "'TT'" := truep : PropositionalLogic. + +Local Open Scope logic_base. +Local Open Scope PropositionalLogic. + +Definition orp_witnessed {L: Language} {nL: NormalLanguage L} {pL: PropositionalLanguage L} {Gamma: ProofTheory L}: context -> Prop := + fun Phi => forall x y, Phi (x || y) -> Phi x \/ Phi y. + +Module PropositionalLanguage. + +Inductive expr {Var: Type}: Type := + | andp : expr -> expr -> expr + | orp : expr -> expr -> expr + | impp : expr -> expr -> expr + | falsep : expr + | varp : Var -> expr. + +Implicit Arguments expr. + +Instance L (Var: Type): Language := + Build_Language (expr Var). + +Instance nL (Var: Type): NormalLanguage (L Var) := + Build_NormalLanguage (L Var) impp. + +Instance pL (Var: Type): PropositionalLanguage (L Var) := + Build_PropositionalLanguage (L Var) (nL Var) andp orp falsep. + +Definition rank {Var: Type}: expr Var -> nat := + fix rank (x: expr Var): nat := + match x with + | andp y z => 1 + rank y + rank z + | orp y z => 1 + rank y + rank z + | impp y z => 1 + rank y + rank z + | falsep => 0 + | varp p => 0 + end. + +Definition formula_countable: forall Var, Countable Var -> Countable (expr Var). + intros. + assert (forall n, Countable (sig (fun x: expr Var => rank x <= n))). + + induction n. + - apply (@bijection_Countable _ (Var + unit)%type); [| solve_Countable]. + apply bijection_sym. + apply (FBuild_bijection _ _ (fun x => + match x with + | inl p => exist (fun x: expr Var => rank x <= 0) (varp p) (le_n 0) + | inr _ => exist (fun x: expr Var => rank x <= 0) falsep (le_n 0) + end)). + * hnf; intros. + destruct a1 as [? | []], a2 as [? | []]; inversion H; auto. + * hnf; intros. + destruct b as [[] HH]; try solve [inversion HH]. + 1: exists (inr tt); eauto; f_equal; apply proof_irrelevance. + 1: exists (inl v); eauto; f_equal; apply proof_irrelevance. + - set (s := sig (fun x: expr Var => rank x <= n)). + apply (@injection_Countable _ (s * s + s * s + s * s + unit + Var)%type); [| solve_Countable]. + + apply (Build_injection _ _ (fun x y => + match y with + | inl (inl (inl (inl (exist _ y _, exist _ z _)))) => proj1_sig x = andp y z + | inl (inl (inl (inr (exist _ y _, exist _ z _)))) => proj1_sig x = orp y z + | inl (inl (inr (exist _ y _, exist _ z _))) => proj1_sig x = impp y z + | inl (inr _) => proj1_sig x = falsep + | inr p => proj1_sig x = varp p + end)). + * hnf; intros. + destruct a as [[y z | y z | y z | | p] ?H]. + (* 1 *) simpl in H. assert (rank y <= n) by omega. assert (rank z <= n) by omega. + exists (inl (inl (inl (inl (exist _ y H0, exist _ z H1))))); auto. + (* 2 *) simpl in H. assert (rank y <= n) by omega. assert (rank z <= n) by omega. + exists (inl (inl (inl (inr (exist _ y H0, exist _ z H1))))); auto. + (* 3 *) simpl in H. assert (rank y <= n) by omega. assert (rank z <= n) by omega. + exists (inl (inl (inr (exist _ y H0, exist _ z H1)))); auto. + (* 4 *) exists (inl (inr tt)); auto. + (* 5 *) exists (inr p); auto. + * hnf; intros. + destruct a as [[y z | y z | y z | | p] ?H]; + destruct b1 as [[[[[[y1 ?H] [z1 ?H]] | [[y1 ?H] [z1 ?H]]] | [[y1 ?H] [z1 ?H]]] |] | p1]; try solve [inversion H]; + destruct b2 as [[[[[[y2 ?H] [z2 ?H]] | [[y2 ?H] [z2 ?H]]] | [[y2 ?H] [z2 ?H]]] |] | p2]; try solve [inversion H0]. + (* 1 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance. + (* 2 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance. + (* 3 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance. + (* 4 *) destruct u, u0; auto. + (* 5 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance. + * hnf; intros. + destruct b as [[[[[[y ?H] [z ?H]] | [[y ?H] [z ?H]]] | [[y ?H] [z ?H]]] |] | p]; + destruct a1 as [[y1 z1 | y1 z1 | y1 z1 | | p1] ?H]; try solve [inversion H]; + destruct a2 as [[y2 z2 | y2 z2 | y2 z2 | | p2] ?H]; try solve [inversion H0]. + (* 1 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance. + (* 2 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance. + (* 3 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance. + (* 4 *) f_equal; apply proof_irrelevance. + (* 5 *) inversion H; inversion H0; subst; subst; repeat f_equal; apply proof_irrelevance. + + apply (@injection_Countable _ (sigT (fun n => sig (fun x: expr Var => rank x <= n)))); [| solve_Countable; auto]. + apply (FBuild_injection _ _ (fun x0 => existT (fun n => sig (fun x => rank x <= n)) (rank x0) (exist (fun x => rank x <= rank x0) x0 (le_n (rank x0))))). + hnf; intros. + simpl in H. + inversion H; auto. +Qed. (* 20 seconds *) + +End PropositionalLanguage. + diff --git a/SeparationLogic/Downwards2Upwards.v b/SeparationLogic/Downwards2Upwards.v index 2223173..fe56a91 100644 --- a/SeparationLogic/Downwards2Upwards.v +++ b/SeparationLogic/Downwards2Upwards.v @@ -1,60 +1,72 @@ -Require Import Coq.Logic.Classical_Prop. -Require Import Logic.lib.Coqlib. -Require Import Logic.MinimunLogic.LogicBase. -Require Import Logic.MinimunLogic.MinimunLogic. -Require Import Logic.PropositionalLogic.Syntax. -Require Import Logic.SeparationLogic.Syntax. -Require Import Logic.PropositionalLogic.KripkeSemantics. -Require Import Logic.SeparationLogic.DownwardsSemantics. -Require Import Logic.SeparationLogic.UpwardsSemantics. - -Local Open Scope logic_base. -Local Open Scope PropositionalLogic. -Local Open Scope SeparationLogic. - -Definition d2u_sSM {L: Language} {nL: NormalLanguage L} {pL: PropositionalLanguage L} {SL: SeparationLanguage L} {SM: Semantics L} {pkSM: PreKripkeSemantics L SM} {kiSM: KripkeIntuitionisticSemantics L SM} (dsSM: DownwardsSemantics L SM): UpwardsSemantics L SM. - refine (Build_UpwardsSemantics _ _ _ _ _ _ _ (fun M (m1 m2 m: Kworlds M) => exists n1 n2, Korder n1 m1 /\ Korder n2 m2 /\ DownwardsSemantics.join n1 n2 m) _ _ _ _ _). - + (* join_comm *) - intros. - destruct H as [n1 [n2 [? [? ?]]]]. - exists n2, n1. - split; [| split]; auto. - apply DownwardsSemantics.join_comm; auto. - + (* join_assoc *) - admit. - + (* join_Korder *) - intros. - pose proof Korder_PreOrder M as H_PreOrder. - exists m. - split; [| reflexivity]. - destruct H as [m1' [m2' [? [? ?]]]]. - exists m1', m2'. - split; [| split]; auto; etransitivity; eauto. - + (* sat_sepcon *) - intros. - pose proof Korder_PreOrder M as H_PreOrder. - rewrite DownwardsSemantics.sat_sepcon. - split; intros. - - destruct H as [m1 [m2 [? [? ?]]]]. - exists m, m1, m2. - split; [reflexivity |]. - split; [| split]; auto. - exists m1, m2. - split; [| split]; auto; reflexivity. - - destruct H as [m0 [m1 [m2 [? [[n1 [n2 [? [? ?]]]] [? ?]]]]]]. - destruct (DownwardsSemantics.join_Korder M m0 m _ _ H2 H) as [n1' [n2' [? [? ?]]]]. - exists n1', n2'. - split; [| split]; auto; eapply sat_mono; eauto; eapply sat_mono; eauto. - + (* sat_wand *) - intros. - pose proof Korder_PreOrder M as H_PreOrder. - rewrite DownwardsSemantics.sat_wand. - split; intros. - - destruct H0 as [m' [m1' [? [? ?]]]]. - apply (H _ _ _ H0 H3). - eapply sat_mono; eauto. - - apply (H m1 m2); auto. - exists m0, m1. - split; [| split]; auto. - reflexivity. -Defined. +Require Import Coq.Logic.Classical_Prop. +Require Import Logic.lib.Coqlib. +Require Import Logic.MinimunLogic.LogicBase. +Require Import Logic.MinimunLogic.MinimunLogic. +Require Import Logic.PropositionalLogic.Syntax. +Require Import Logic.SeparationLogic.Syntax. +Require Import Logic.PropositionalLogic.KripkeSemantics. +Require Import Logic.SeparationLogic.DownwardsSemantics. +Require Import Logic.SeparationLogic.UpwardsSemantics. + +Local Open Scope logic_base. +Local Open Scope PropositionalLogic. +Local Open Scope SeparationLogic. + +Definition d2u_sSM {L: Language} {nL: NormalLanguage L} {pL: PropositionalLanguage L} {SL: SeparationLanguage L} {SM: Semantics L} {pkSM: PreKripkeSemantics L SM} {kiSM: KripkeIntuitionisticSemantics L SM} (dsSM: DownwardsSemantics L SM): UpwardsSemantics L SM. + refine (Build_UpwardsSemantics _ _ _ _ _ _ _ (fun M (m1 m2 m: Kworlds M) => exists n1 n2, Korder n1 m1 /\ Korder n2 m2 /\ DownwardsSemantics.join n1 n2 m) _ _ _ _ _). + + (* join_comm *) + intros. + destruct H as [n1 [n2 [? [? ?]]]]. + exists n2, n1. + split; [| split]; auto. + apply DownwardsSemantics.join_comm; auto. + + (* join_assoc *) + intros. + pose proof Korder_PreOrder M as H_PreOrder. + destruct H as [mx'' [my'' [? [? ?]]]]. + destruct H0 as [mxy' [mz' [? [? ?]]]]. + destruct (DownwardsSemantics.join_Korder M _ _ _ _ H2 H0) as [mx' [my' [? [? ?]]]]. + destruct (DownwardsSemantics.join_assoc M _ _ _ _ _ H5 H4) as [myz' [? ?]]. + exists myz'. + split. + - exists my', mz'; split; [| split]; auto. + etransitivity; eauto. + - exists mx', myz'; split; [| split]; auto. + * etransitivity; eauto. + * reflexivity. + + (* join_Korder *) + intros. + pose proof Korder_PreOrder M as H_PreOrder. + exists m. + split; [| reflexivity]. + destruct H as [m1' [m2' [? [? ?]]]]. + exists m1', m2'. + split; [| split]; auto; etransitivity; eauto. + + (* sat_sepcon *) + intros. + pose proof Korder_PreOrder M as H_PreOrder. + rewrite DownwardsSemantics.sat_sepcon. + split; intros. + - destruct H as [m1 [m2 [? [? ?]]]]. + exists m, m1, m2. + split; [reflexivity |]. + split; [| split]; auto. + exists m1, m2. + split; [| split]; auto; reflexivity. + - destruct H as [m0 [m1 [m2 [? [[n1 [n2 [? [? ?]]]] [? ?]]]]]]. + destruct (DownwardsSemantics.join_Korder M m0 m _ _ H2 H) as [n1' [n2' [? [? ?]]]]. + exists n1', n2'. + split; [| split]; auto; eapply sat_mono; eauto; eapply sat_mono; eauto. + + (* sat_wand *) + intros. + pose proof Korder_PreOrder M as H_PreOrder. + rewrite DownwardsSemantics.sat_wand. + split; intros. + - destruct H0 as [m' [m1' [? [? ?]]]]. + apply (H _ _ _ H0 H3). + eapply sat_mono; eauto. + - apply (H m1 m2); auto. + exists m0, m1. + split; [| split]; auto. + reflexivity. +Defined. diff --git a/_CoqProject b/_CoqProject new file mode 100644 index 0000000..0879816 --- /dev/null +++ b/_CoqProject @@ -0,0 +1 @@ +-R . Logic diff --git a/lib/Bijection.v b/lib/Bijection.v index 908b6b1..4e70f96 100644 --- a/lib/Bijection.v +++ b/lib/Bijection.v @@ -1,269 +1,272 @@ -Require Export Coq.Relations.Relation_Definitions. -Require Export Coq.Relations.Relation_Operators. -Require Export Coq.Relations.Relation_Definitions. -Require Export Coq.Classes.RelationClasses. -Require Import Omega. - -Definition image_defined {A B} (R: A -> B -> Prop): Prop := - forall a, exists b, R a b. - -Definition partial_functional {A B} (R: A -> B -> Prop): Prop := - forall a b1 b2, R a b1 -> R a b2 -> b1 = b2. - -Definition injective {A B} (R: A -> B -> Prop): Prop := - forall a1 a2 b, R a1 b -> R a2 b -> a1 = a2. - -Definition surjective {A B} (R: A -> B -> Prop): Prop := - forall b, exists a, R a b. - -Definition function_injective {A B} (f: A -> B): Prop := - forall a1 a2, f a1 = f a2 -> a1 = a2. - -Definition function_surjective {A B} (f: A -> B): Prop := - forall b, exists a, f a = b. - -Record injection (A B: Type): Type := { - inj_R:> A -> B -> Prop; - im_inj: image_defined inj_R; - pf_inj: partial_functional inj_R; - in_inj: injective inj_R -}. - -Record surjection (A B: Type): Type := { - sur_R:> A -> B -> Prop; - im_surj: image_defined sur_R; - pf_surj: partial_functional sur_R; - su_surj: surjective sur_R -}. - -Record bijection (A B: Type): Type := { - bij_R:> A -> B -> Prop; - im_bij: image_defined bij_R; - pf_bij: partial_functional bij_R; - in_bij: injective bij_R; - su_bij: surjective bij_R -}. - -Definition FBuild_injection (A B: Type) (f: A -> B) (H: function_injective f): injection A B. - apply (Build_injection _ _ (fun a b => f a = b)). - + hnf; intros; eauto. - + hnf; intros; congruence. - + hnf; intros. - apply H; congruence. -Defined. - -Definition FBuild_surjection (A B: Type) (f: A -> B) (H: function_surjective f): surjection A B. - apply (Build_surjection _ _ (fun a b => f a = b)). - + hnf; intros; eauto. - + hnf; intros; congruence. - + hnf; intros. - apply H; congruence. -Defined. - -Definition FBuild_bijection (A B: Type) (f: A -> B) (H: function_injective f) (H0: function_surjective f): bijection A B. - apply (Build_bijection _ _ (fun a b => f a = b)). - + hnf; intros; eauto. - + hnf; intros; congruence. - + hnf; intros. - apply H; congruence. - + hnf; intros. - apply H0. -Defined. - -Definition injection_trans {A B C} (R1: injection A B) (R2: injection B C): injection A C. - intros. - apply (Build_injection _ _ (fun a c => exists b, R1 a b /\ R2 b c)). - + hnf; intros. - destruct (im_inj _ _ R1 a) as [b ?]. - destruct (im_inj _ _ R2 b) as [c ?]. - exists c; eauto. - + hnf; intros a c1 c2 [b1 [? ?]] [b2 [? ?]]. - pose proof pf_inj _ _ R1 a b1 b2 H H1. - subst b2. - pose proof pf_inj _ _ R2 b1 c1 c2 H0 H2. - auto. - + hnf; intros a1 a2 c [b1 [? ?]] [b2 [? ?]]. - pose proof in_inj _ _ R2 b1 b2 c H0 H2. - subst b2. - pose proof in_inj _ _ R1 a1 a2 b1 H H1. - auto. -Defined. - -Definition bijection_sym {A B} (R: bijection A B): bijection B A. - apply (Build_bijection _ _ (fun a b => R b a)). - + hnf. - apply (su_bij _ _ R). - + hnf; intros. - apply (in_bij _ _ R b1 b2 a); auto. - + hnf; intros. - apply (pf_bij _ _ R b a1 a2); auto. - + hnf. - apply (im_bij _ _ R). -Qed. - -Definition sum_injection {A1 B1 A2 B2} (R1: injection A1 B1) (R2: injection A2 B2): injection (sum A1 A2) (sum B1 B2). -Proof. - intros. - apply (Build_injection _ _ (fun a b => - match a, b with - | inl a, inl b => R1 a b - | inr a, inr b => R2 a b - | _, _ => False - end)). - + hnf; intros. - destruct a as [a | a]. - - destruct (im_inj _ _ R1 a) as [b ?]. - exists (inl b); auto. - - destruct (im_inj _ _ R2 a) as [b ?]. - exists (inr b); auto. - + hnf; intros. - destruct a as [a | a], b1 as [b1 | b1], b2 as [b2 | b2]; try solve [inversion H | inversion H0]. - - f_equal; apply (pf_inj _ _ R1 a); auto. - - f_equal; apply (pf_inj _ _ R2 a); auto. - + hnf; intros. - destruct a1 as [a1 | a1], a2 as [a2 | a2], b as [b | b]; try solve [inversion H | inversion H0]. - - f_equal; apply (in_inj _ _ R1 _ _ b); auto. - - f_equal; apply (in_inj _ _ R2 _ _ b); auto. -Qed. - -Definition prod_injection {A1 B1 A2 B2} (R1: injection A1 B1) (R2: injection A2 B2): injection (prod A1 A2) (prod B1 B2). -Proof. - intros. - apply (Build_injection _ _ (fun a b => R1 (fst a) (fst b) /\ R2 (snd a) (snd b))). - + hnf; intros. - destruct (im_inj _ _ R1 (fst a)) as [b1 ?]. - destruct (im_inj _ _ R2 (snd a)) as [b2 ?]. - exists (b1, b2); auto. - + hnf; intros. - destruct b1, b2, H, H0. - pose proof pf_inj _ _ R1 (fst a) _ _ H H0. - pose proof pf_inj _ _ R2 (snd a) _ _ H1 H2. - simpl in *; subst; auto. - + hnf; intros. - destruct a1, a2, H, H0. - pose proof in_inj _ _ R1 _ _ _ H H0. - pose proof in_inj _ _ R2 _ _ _ H1 H2. - simpl in *; subst; auto. -Qed. - -Definition sigT_injection (I: Type) (A: I -> Type) (B: Type) (R: forall i: I, injection (A i) B): injection (sigT A) (I * B). - apply (Build_injection _ _ (fun a b => projT1 a = fst b /\ (R (projT1 a)) (projT2 a) (snd b))). - + hnf; intros. - destruct a as [i a0]. - destruct (im_inj _ _ (R i) a0) as [b0 ?]. - exists (i, b0). - auto. - + hnf; intros. - destruct b1 as [i1 b1]; simpl in H. - destruct b2 as [i2 b2]; simpl in H0. - destruct H, H0; subst. - pose proof pf_inj _ _ (R (projT1 a)) _ _ _ H1 H2. - subst; auto. - + hnf; intros. - destruct b, H, H0; simpl in *; subst. - destruct a1, a2; simpl in *; subst. - pose proof in_inj _ _ (R x) _ _ _ H1 H2. - subst; auto. -Qed. - -Definition bijection_injection {A B} (R: bijection A B): injection A B := - Build_injection _ _ R (im_bij _ _ R) (pf_bij _ _ R) (in_bij _ _ R). - -Definition nat2_nat_bijection: bijection (sum nat nat) nat. - apply (Build_bijection _ _ (fun n m => match n with | inl n => m = n + n | inr n => m = n + n +1 end)). - + hnf; intros. - destruct a; eauto. - + hnf; intros. - destruct a; inversion H; inversion H0; auto. - + hnf; intros. - destruct a1, a2; inversion H; inversion H0; destruct (lt_eq_lt_dec n n0) as [[? | ?] | ?]; try omega; subst; auto. - + hnf; intros. - destruct (Even.even_odd_dec b) as [H | H]. - - rewrite (proj1 (Div2.even_odd_double _)), NPeano.double_twice in H. - exists (inl (Div2.div2 b)). - rewrite H at 1. omega. - - rewrite (proj2 (Div2.even_odd_double _)), NPeano.double_twice in H. - exists (inr (Div2.div2 b)). - rewrite H at 1. omega. -Qed. - -Definition natnat_nat_bijection: bijection (prod nat nat) nat. - apply (Build_bijection _ _ - (fun n m => m = match n with | (n1, n2) => - (fix sum (x: nat): nat := match x with | O => O | S x => S x + sum x end) - (n1 + n2) - + n1 - end)). - + hnf; intros. - destruct a; eauto. - + hnf; intros. - destruct a; omega. - + hnf; intros. - destruct a1 as [a11 a12], a2 as [a21 a22]. - assert (forall m1 m2, m1 < m2 -> - (fix sum (x : nat) : nat := - match x with - | 0 => 0 - | S x0 => S x0 + sum x0 - end) m1 + m1 < - (fix sum (x : nat) : nat := - match x with - | 0 => 0 - | S x0 => S x0 + sum x0 - end) m2). - Focus 1. { - intros. - remember (m2 - m1 - 1) as d; assert (m2 = (S d) + m1) by omega. - subst m2; clear. - induction d. - + simpl. - omega. - + simpl in *. - omega. - } Unfocus. - destruct (lt_eq_lt_dec (a11 + a12) (a21 + a22)) as [[HH | HH] | HH]. - - specialize (H1 _ _ HH). - omega. - - rewrite HH in H. - assert (a11 = a21) by omega. - assert (a12 = a22) by omega. - subst; auto. - - specialize (H1 _ _ HH). - omega. - + hnf; intros. - assert (exists s, - (fix sum (x : nat) : nat := - match x with - | 0 => 0 - | S x0 => S x0 + sum x0 - end) s <= b < - (fix sum (x : nat) : nat := - match x with - | 0 => 0 - | S x0 => S x0 + sum x0 - end) (S s)). - Focus 1. { - induction b. - + exists 0; simpl. - omega. - + destruct IHb as [s ?]. - remember (b - (fix sum (x : nat) : nat := - match x with - | 0 => 0 - | S x0 => S x0 + sum x0 - end) s) as d. - destruct (lt_dec d s) as [HH | HH]. - - exists s; simpl in *; omega. - - exists (S s); simpl in *; omega. - } Unfocus. - destruct H as [s ?]. - remember (b - (fix sum (x : nat) : nat := - match x with - | 0 => 0 - | S x0 => S x0 + sum x0 - end) s) as a1. - exists (a1, s - a1). - replace (a1 + (s - a1)) with s by omega. - omega. -Qed. - +Require Export Coq.Relations.Relation_Definitions. +Require Export Coq.Relations.Relation_Operators. +Require Export Coq.Relations.Relation_Definitions. +Require Export Coq.Classes.RelationClasses. +Require Import Coq.Arith.Even. +Require Import Coq.Arith.Div2. +Require Import Coq.Numbers.Natural.Peano.NPeano. +Require Import Omega. + +Definition image_defined {A B} (R: A -> B -> Prop): Prop := + forall a, exists b, R a b. + +Definition partial_functional {A B} (R: A -> B -> Prop): Prop := + forall a b1 b2, R a b1 -> R a b2 -> b1 = b2. + +Definition injective {A B} (R: A -> B -> Prop): Prop := + forall a1 a2 b, R a1 b -> R a2 b -> a1 = a2. + +Definition surjective {A B} (R: A -> B -> Prop): Prop := + forall b, exists a, R a b. + +Definition function_injective {A B} (f: A -> B): Prop := + forall a1 a2, f a1 = f a2 -> a1 = a2. + +Definition function_surjective {A B} (f: A -> B): Prop := + forall b, exists a, f a = b. + +Record injection (A B: Type): Type := { + inj_R:> A -> B -> Prop; + im_inj: image_defined inj_R; + pf_inj: partial_functional inj_R; + in_inj: injective inj_R +}. + +Record surjection (A B: Type): Type := { + sur_R:> A -> B -> Prop; + im_surj: image_defined sur_R; + pf_surj: partial_functional sur_R; + su_surj: surjective sur_R +}. + +Record bijection (A B: Type): Type := { + bij_R:> A -> B -> Prop; + im_bij: image_defined bij_R; + pf_bij: partial_functional bij_R; + in_bij: injective bij_R; + su_bij: surjective bij_R +}. + +Definition FBuild_injection (A B: Type) (f: A -> B) (H: function_injective f): injection A B. + apply (Build_injection _ _ (fun a b => f a = b)). + + hnf; intros; eauto. + + hnf; intros; congruence. + + hnf; intros. + apply H; congruence. +Defined. + +Definition FBuild_surjection (A B: Type) (f: A -> B) (H: function_surjective f): surjection A B. + apply (Build_surjection _ _ (fun a b => f a = b)). + + hnf; intros; eauto. + + hnf; intros; congruence. + + hnf; intros. + apply H; congruence. +Defined. + +Definition FBuild_bijection (A B: Type) (f: A -> B) (H: function_injective f) (H0: function_surjective f): bijection A B. + apply (Build_bijection _ _ (fun a b => f a = b)). + + hnf; intros; eauto. + + hnf; intros; congruence. + + hnf; intros. + apply H; congruence. + + hnf; intros. + apply H0. +Defined. + +Definition injection_trans {A B C} (R1: injection A B) (R2: injection B C): injection A C. + intros. + apply (Build_injection _ _ (fun a c => exists b, R1 a b /\ R2 b c)). + + hnf; intros. + destruct (im_inj _ _ R1 a) as [b ?]. + destruct (im_inj _ _ R2 b) as [c ?]. + exists c; eauto. + + hnf; intros a c1 c2 [b1 [? ?]] [b2 [? ?]]. + pose proof pf_inj _ _ R1 a b1 b2 H H1. + subst b2. + pose proof pf_inj _ _ R2 b1 c1 c2 H0 H2. + auto. + + hnf; intros a1 a2 c [b1 [? ?]] [b2 [? ?]]. + pose proof in_inj _ _ R2 b1 b2 c H0 H2. + subst b2. + pose proof in_inj _ _ R1 a1 a2 b1 H H1. + auto. +Defined. + +Definition bijection_sym {A B} (R: bijection A B): bijection B A. + apply (Build_bijection _ _ (fun a b => R b a)). + + hnf. + apply (su_bij _ _ R). + + hnf; intros. + apply (in_bij _ _ R b1 b2 a); auto. + + hnf; intros. + apply (pf_bij _ _ R b a1 a2); auto. + + hnf. + apply (im_bij _ _ R). +Qed. + +Definition sum_injection {A1 B1 A2 B2} (R1: injection A1 B1) (R2: injection A2 B2): injection (sum A1 A2) (sum B1 B2). +Proof. + intros. + apply (Build_injection _ _ (fun a b => + match a, b with + | inl a, inl b => R1 a b + | inr a, inr b => R2 a b + | _, _ => False + end)). + + hnf; intros. + destruct a as [a | a]. + - destruct (im_inj _ _ R1 a) as [b ?]. + exists (inl b); auto. + - destruct (im_inj _ _ R2 a) as [b ?]. + exists (inr b); auto. + + hnf; intros. + destruct a as [a | a], b1 as [b1 | b1], b2 as [b2 | b2]; try solve [inversion H | inversion H0]. + - f_equal; apply (pf_inj _ _ R1 a); auto. + - f_equal; apply (pf_inj _ _ R2 a); auto. + + hnf; intros. + destruct a1 as [a1 | a1], a2 as [a2 | a2], b as [b | b]; try solve [inversion H | inversion H0]. + - f_equal; apply (in_inj _ _ R1 _ _ b); auto. + - f_equal; apply (in_inj _ _ R2 _ _ b); auto. +Qed. + +Definition prod_injection {A1 B1 A2 B2} (R1: injection A1 B1) (R2: injection A2 B2): injection (prod A1 A2) (prod B1 B2). +Proof. + intros. + apply (Build_injection _ _ (fun a b => R1 (fst a) (fst b) /\ R2 (snd a) (snd b))). + + hnf; intros. + destruct (im_inj _ _ R1 (fst a)) as [b1 ?]. + destruct (im_inj _ _ R2 (snd a)) as [b2 ?]. + exists (b1, b2); auto. + + hnf; intros. + destruct b1, b2, H, H0. + pose proof pf_inj _ _ R1 (fst a) _ _ H H0. + pose proof pf_inj _ _ R2 (snd a) _ _ H1 H2. + simpl in *; subst; auto. + + hnf; intros. + destruct a1, a2, H, H0. + pose proof in_inj _ _ R1 _ _ _ H H0. + pose proof in_inj _ _ R2 _ _ _ H1 H2. + simpl in *; subst; auto. +Qed. + +Definition sigT_injection (I: Type) (A: I -> Type) (B: Type) (R: forall i: I, injection (A i) B): injection (sigT A) (I * B). + apply (Build_injection _ _ (fun a b => projT1 a = fst b /\ (R (projT1 a)) (projT2 a) (snd b))). + + hnf; intros. + destruct a as [i a0]. + destruct (im_inj _ _ (R i) a0) as [b0 ?]. + exists (i, b0). + auto. + + hnf; intros. + destruct b1 as [i1 b1]; simpl in H. + destruct b2 as [i2 b2]; simpl in H0. + destruct H, H0; subst. + pose proof pf_inj _ _ (R (projT1 a)) _ _ _ H1 H2. + subst; auto. + + hnf; intros. + destruct b, H, H0; simpl in *; subst. + destruct a1, a2; simpl in *; subst. + pose proof in_inj _ _ (R x) _ _ _ H1 H2. + subst; auto. +Qed. + +Definition bijection_injection {A B} (R: bijection A B): injection A B := + Build_injection _ _ R (im_bij _ _ R) (pf_bij _ _ R) (in_bij _ _ R). + +Definition nat2_nat_bijection: bijection (sum nat nat) nat. + apply (Build_bijection _ _ (fun n m => match n with | inl n => m = n + n | inr n => m = n + n +1 end)). + + hnf; intros. + destruct a; eauto. + + hnf; intros. + destruct a; inversion H; inversion H0; auto. + + hnf; intros. + destruct a1, a2; inversion H; inversion H0; destruct (lt_eq_lt_dec n n0) as [[? | ?] | ?]; try omega; subst; auto. + + hnf; intros. + destruct (Even.even_odd_dec b) as [H | H]. + - rewrite (proj1 (Div2.even_odd_double _)), NPeano.double_twice in H. + exists (inl (Div2.div2 b)). + rewrite H at 1. omega. + - rewrite (proj2 (Div2.even_odd_double _)), NPeano.double_twice in H. + exists (inr (Div2.div2 b)). + rewrite H at 1. omega. +Qed. + +Definition natnat_nat_bijection: bijection (prod nat nat) nat. + apply (Build_bijection _ _ + (fun n m => m = match n with | (n1, n2) => + (fix sum (x: nat): nat := match x with | O => O | S x => S x + sum x end) + (n1 + n2) + + n1 + end)). + + hnf; intros. + destruct a; eauto. + + hnf; intros. + destruct a; omega. + + hnf; intros. + destruct a1 as [a11 a12], a2 as [a21 a22]. + assert (forall m1 m2, m1 < m2 -> + (fix sum (x : nat) : nat := + match x with + | 0 => 0 + | S x0 => S x0 + sum x0 + end) m1 + m1 < + (fix sum (x : nat) : nat := + match x with + | 0 => 0 + | S x0 => S x0 + sum x0 + end) m2). + Focus 1. { + intros. + remember (m2 - m1 - 1) as d; assert (m2 = (S d) + m1) by omega. + subst m2; clear. + induction d. + + simpl. + omega. + + simpl in *. + omega. + } Unfocus. + destruct (lt_eq_lt_dec (a11 + a12) (a21 + a22)) as [[HH | HH] | HH]. + - specialize (H1 _ _ HH). + omega. + - rewrite HH in H. + assert (a11 = a21) by omega. + assert (a12 = a22) by omega. + subst; auto. + - specialize (H1 _ _ HH). + omega. + + hnf; intros. + assert (exists s, + (fix sum (x : nat) : nat := + match x with + | 0 => 0 + | S x0 => S x0 + sum x0 + end) s <= b < + (fix sum (x : nat) : nat := + match x with + | 0 => 0 + | S x0 => S x0 + sum x0 + end) (S s)). + Focus 1. { + induction b. + + exists 0; simpl. + omega. + + destruct IHb as [s ?]. + remember (b - (fix sum (x : nat) : nat := + match x with + | 0 => 0 + | S x0 => S x0 + sum x0 + end) s) as d. + destruct (lt_dec d s) as [HH | HH]. + - exists s; simpl in *; omega. + - exists (S s); simpl in *; omega. + } Unfocus. + destruct H as [s ?]. + remember (b - (fix sum (x : nat) : nat := + match x with + | 0 => 0 + | S x0 => S x0 + sum x0 + end) s) as a1. + exists (a1, s - a1). + replace (a1 + (s - a1)) with s by omega. + omega. +Qed. +