From Equations Require Import Equations.
From Coq Require Import Arith Lia List Program.Equality.
From Undecidability.FOL Require Import FullSyntax Heyting.Heyting Completeness.HeytingMacNeille.
Import ListNotations.
Section Lindenbaum.
Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
Context {eq_dec_Funcs : EqDec Σ_funcs}.
Context {eq_dec_Preds : EqDec Σ_preds}.
Section Completeness.
Notation "A ⊢E phi" := (A ⊢I phi) (at level 30).
Instance lb_alg : HeytingAlgebra.
Proof.
unshelve eapply (@Build_HeytingAlgebra (@form _ _ _ falsity_on)).
- intros phi psi. exact ([phi] ⊢E psi).
- exact ⊥.
- intros phi psi. exact (phi ∧ psi).
- intros phi psi. exact (phi ∨ psi).
- intros phi psi. exact (phi → psi).
- intros phi. apply Ctx. now left.
- intros phi psi theta H1 H2. apply IE with (phi:=psi); trivial.
apply Weak with (A:=[]); auto. 2: firstorder. econstructor. apply H2.
- intros phi. cbn. apply Exp, Ctx. now left.
- intros phi psi theta. cbn. split.
+ intros [H1 H2]. now apply CI.
+ intros H. split; [apply (CE1 H) | apply (CE2 H)].
- intros phi psi theta. cbn. split.
+ intros [H1 H2]. eapply DE. apply Ctx; auto. 1: now left.
eapply Weak. exact H1. firstorder.
eapply Weak. exact H2. firstorder.
+ intros H; split.
* apply (IE (phi := phi ∨ psi)). 2: try apply DI1, Ctx. 2: now left.
apply II. eapply Weak; eauto. 1: firstorder.
* apply (IE (phi := phi ∨ psi)); try apply DI2, Ctx; try now left.
apply II. eapply Weak; eauto. firstorder.
- intros phi psi theta. cbn. split.
+ intros H. apply II. apply (IE (phi := theta ∧ phi)).
* apply II. eapply Weak. 1: apply H. firstorder.
* apply CI; apply Ctx; firstorder.
+ intros H. eapply IE. 2: eapply CE2, Ctx; now left.
eapply IE. 1: eapply II, Weak. 1: apply H. 2: eapply CE1, Ctx; now left. firstorder.
Defined.
Lemma lb_alg_iff phi :
Top <= phi <-> [] ⊢E phi.
Proof.
cbn. split; intros H.
- apply (IE (phi := ¬ ⊥)); apply II; eauto using Ctx. apply Ctx. now left.
- eapply Weak; eauto; firstorder.
Qed.
Instance lb_calg : CompleteHeytingAlgebra :=
@completion_calgebra lb_alg.
Definition lb_Pr P v : lb_calg :=
embed (atom P v).
Lemma lindenbaum_hsat phi :
down phi ≡ proj1_sig (hsat lb_Pr phi).
Proof.
induction phi as [| |[]|[]] using form_ind_subst; simp hsat in *.
- rewrite down_bot. reflexivity.
- cbn. reflexivity.
- rewrite (@down_meet lb_alg f1 f2), IHphi, IHphi0. now destruct hsat, hsat.
- rewrite (@down_join lb_alg f1 f2), IHphi, IHphi0. now destruct hsat, hsat.
- rewrite (@down_impl lb_alg f1 f2), IHphi, IHphi0. now destruct hsat, hsat.
- cbn. split; intros psi H'.
+ intros X [HX [t Ht]]. change (psi ∈ proj1_sig (exist normal X HX)).
eapply Ht. rewrite <- H. apply AllE, H'.
+ apply AllI. destruct (@nameless_equiv_all _ _ _ intu ([psi]) f2) as [t Ht]. apply Ht.
apply H, H'. exists (proj2_sig (hsat lb_Pr f2[t..])), t. now destruct hsat.
- cbn. split; intros psi H'.
+ intros X [XD HX]. apply XD. intros theta HT. apply (ExE H').
destruct (@nameless_equiv_ex _ _ _ intu ([psi]) f2 theta) as [t Ht]. apply Ht.
assert (exists i : term, equiv_HA (hsat lb_Pr f2[t..]) (hsat lb_Pr f2[i..])) by now eexists.
specialize (HX (hsat lb_Pr f2[t..]) H0).
apply Weak with (A:=[f2[t..]]); auto. 2: now apply ListAutomation.incl_shift.
apply HT, HX. rewrite <- H. apply Ctx. now left.
+ specialize (H' (down (∃ f2))). apply H'.
exists (@down_normal lb_alg (∃ f2)). intros X [t ?].
intros ? ?. eapply H0 in H1.
revert x H1. fold (hset_sub (proj1_sig (hsat lb_Pr f2[t..])) (down (∃ f2))).
rewrite <- H. apply down_mono. eapply ExI, Ctx; eauto. now left.
Qed.
Lemma lindenbaum_eqH phi :
eqH (embed phi) (hsat lb_Pr phi).
Proof.
unfold eqH. cbn. now rewrite <- lindenbaum_hsat.
Qed.
Lemma lb_calg_iff phi :
Top <= hsat lb_Pr phi <-> nil ⊢E phi.
Proof.
cbn. rewrite <- lindenbaum_hsat.
rewrite <- down_top, <- lb_alg_iff. split.
- apply down_inj.
- apply down_mono.
Qed.
End Completeness.
Definition hvalid phi :=
forall (HA : CompleteHeytingAlgebra) HP, Top <= hsat HP phi.
Theorem hcompleteness phi :
hvalid phi -> nil ⊢I phi.
Proof.
intros H.
specialize (H lb_calg lb_Pr).
now eapply lb_calg_iff.
Unshelve.
Qed.
Section Completeness.
Variable gprv : list form -> form -> Prop.
Notation "A ⊢ phi" := (gprv A phi) (at level 55).
Hypothesis gCtx : forall A phi, In phi A -> A ⊢ phi.
Hypothesis gIE : forall A phi psi, A ⊢ (phi → psi) -> A ⊢ phi -> A ⊢ psi.
Hypothesis gII : forall A phi psi, (phi::A) ⊢ psi -> A ⊢ (phi → psi).
Hypothesis gExp : forall A phi, A ⊢ ⊥ -> A ⊢ phi.
Hypothesis gCI : forall A phi psi, A ⊢ phi -> A ⊢ psi -> A ⊢ (phi ∧ psi).
Hypothesis gCE1 : forall A phi psi, A ⊢ (phi ∧ psi) -> A ⊢ phi.
Hypothesis gCE2 : forall A phi psi, A ⊢ (phi ∧ psi) -> A ⊢ psi.
Hypothesis gDI1 : forall A phi psi, A ⊢ phi -> A ⊢ (phi ∨ psi).
Hypothesis gDI2 : forall A phi psi, A ⊢ psi -> A ⊢ (phi ∨ psi).
Hypothesis gDE : forall A phi psi theta, A ⊢ (phi ∨ psi) -> (phi :: A) ⊢ theta -> (psi :: A) ⊢ theta -> A ⊢ theta.
Hypothesis gWeak : forall A B phi, A ⊢ phi -> incl A B -> B ⊢ phi.
Instance glb_alg : HeytingAlgebra.
Proof.
unshelve eapply (@Build_HeytingAlgebra (form)).
- intros phi psi. exact ([phi] ⊢ psi).
- exact ⊥.
- intros phi psi. exact (phi ∧ psi).
- intros phi psi. exact (phi ∨ psi).
- intros phi psi. exact (phi → psi).
- intros phi. apply gCtx. now left.
- intros phi psi theta H1 H2. apply gIE with (phi:=psi); trivial.
apply gWeak with (A:=[]); auto. firstorder.
- intros phi. cbn. apply gExp, gCtx. now left.
- intros phi psi theta. cbn. split.
+ intros [H1 H2]. now apply gCI.
+ intros H. split; [apply (gCE1 H) | apply (gCE2 H)].
- intros phi psi theta. cbn. split.
+ intros [H1 H2]. eapply gDE. apply gCtx; auto. 1: now left.
eapply gWeak. exact H1. firstorder.
eapply gWeak. exact H2. firstorder.
+ intros H; split.
* apply (gIE (phi := phi ∨ psi)); try apply gDI1, gCtx.
apply gII. eapply gWeak; eauto. 1: firstorder. now left.
* apply (gIE (phi := phi ∨ psi)); try apply gDI2, gCtx.
apply gII. eapply gWeak; eauto. 1: firstorder. now left.
- intros phi psi theta. cbn. split.
+ intros H. apply gII. apply (gIE (phi := theta ∧ phi)).
* apply gII. eapply gWeak; eauto. firstorder.
* apply gCI; apply gCtx; auto. 1: right; now left. now left.
+ intros H. apply (gIE (phi:=phi)). 2: eapply gCE2, gCtx; now left.
eapply gIE. 1: eapply gII, gWeak. 1: apply H. 2: eapply gCE1, gCtx; now left.
firstorder.
Defined.
Lemma glb_alg_iff phi :
Top <= phi <-> [] ⊢ phi.
Proof.
cbn. split; intros H.
- apply (gIE (phi := ¬ ⊥)); apply gII. 2: apply gCtx; now left. apply H.
- eapply gWeak; eauto. firstorder.
Qed.
Instance glb_calg : CompleteHeytingAlgebra :=
@completion_calgebra glb_alg.
Definition glb_Pr P v : glb_calg :=
embed (atom P v).
Hypothesis gAllI : forall A phi, map (subst_form ↑) A ⊢ phi -> A ⊢ (∀ phi).
Hypothesis gAllE : forall A t phi, A ⊢ (∀ phi) -> A ⊢ phi[t..].
Hypothesis gExI : forall A t phi, A ⊢ phi[t..] -> A ⊢ (∃ phi).
Hypothesis gExE : forall A phi psi, A ⊢ (∃ phi) -> (phi :: map (subst_form ↑) A) ⊢ psi[↑] -> A ⊢ psi.
Hypothesis gnameless_equiv_all' : forall A phi, exists t, A ⊢ phi[t..] <-> map (subst_form ↑) A ⊢ phi.
Hypothesis gnameless_equiv_ex' : forall A phi psi, exists t, (psi[t..] :: A) ⊢ phi <-> (psi :: map (subst_form ↑) A) ⊢ phi[↑].
Lemma glindenbaum_hsat phi :
down phi ≡ proj1_sig (hsat glb_Pr phi).
Proof.
induction phi as [| |[]phi ? psi ?|[] phi ?] using form_ind_subst; simp hsat in *.
- rewrite down_bot. reflexivity.
- cbn. reflexivity.
- rewrite (@down_meet glb_alg phi psi), IHphi, IHphi0. now destruct hsat, hsat.
- rewrite (@down_join glb_alg phi psi), IHphi, IHphi0. now destruct hsat, hsat.
- rewrite (@down_impl glb_alg phi psi), IHphi, IHphi0. now destruct hsat, hsat.
- cbn. split; intros psi H'.
+ intros X [HX [t Ht]]. change (psi ∈ proj1_sig (exist normal X HX)).
eapply Ht. rewrite <- H. apply gAllE, H'.
+ apply gAllI. destruct (@gnameless_equiv_all' ([psi]) phi) as [t <-].
apply H, H'. exists (proj2_sig (hsat glb_Pr phi[t..])), t. now destruct hsat.
- cbn. split; intros psi H'.
+ intros X [XD HX]. apply XD. intros theta HT. apply (gExE H').
destruct (@gnameless_equiv_ex' ([psi]) theta phi) as [t <-].
assert (exists i : term, equiv_HA (hsat glb_Pr phi[t..]) (hsat glb_Pr phi[i..])) by now eexists.
specialize (HX (hsat glb_Pr phi[t..]) H0).
apply gWeak with (A:=[phi[t..]]); auto.
apply HT, HX. rewrite <- H. apply gCtx. now left. apply ListAutomation.incl_shift. easy.
+ specialize (H' (down (∃ phi))). apply H'.
exists (@down_normal glb_alg (∃ phi)). intros X [t ?].
intros ? ?. eapply H0 in H1.
revert x H1. fold (hset_sub (proj1_sig (hsat glb_Pr phi[t..])) (down (∃ phi))).
rewrite <- H. apply down_mono. eapply gExI, gCtx; eauto. now left.
Qed.
Lemma glindenbaum_eqH phi :
eqH (embed phi) (hsat glb_Pr phi).
Proof.
unfold eqH. cbn. now rewrite <- glindenbaum_hsat.
Qed.
Lemma glb_calg_iff phi :
Top <= hsat glb_Pr phi <-> nil ⊢ phi.
Proof.
cbn. rewrite <- glindenbaum_hsat.
rewrite <- down_top, <- glb_alg_iff. split.
- apply down_inj.
- apply down_mono.
Qed.
End Completeness.
#[local] Hint Constructors prv : core.
Instance clb_alg : HeytingAlgebra.
Proof.
apply (@glb_alg (@prv _ _ _ class)); eauto 2.
apply Weak.
Defined.
Instance clb_calg : CompleteHeytingAlgebra.
Proof.
apply (@glb_calg (@prv _ _ _ class)); eauto 2. apply Weak.
Defined.
Definition clb_Pr P (v : Vector.t term (ar_preds P)) : clb_calg.
Proof.
apply glb_Pr with P. exact v.
Defined.
Lemma clb_alg_boolean :
boolean clb_alg.
Proof.
intros phi psi. cbn. eapply IE; try apply Pc. apply Ctx. now left.
Qed.
Lemma boolean_completion HA :
boolean HA -> boolean (@completion_calgebra HA).
Proof.
intros H. intros [X HX] [Y HY]; cbn. intros a Ha.
unfold hset_impl in Ha. apply HX.
intros b Hb. specialize (Ha (Impl b Bot)).
eapply Rtra; try apply H. apply Impl1, Hb, Ha.
intros c Hc. apply HY. intros d Hd. apply Rtra with Bot; try apply Bot1.
assert (H' : Meet (Impl b Bot) c <= Impl b Bot) by apply Meet2.
apply Impl1 in H'. eapply Rtra; try eassumption. repeat rewrite <- Meet1.
repeat split; auto. eapply Rtra; try apply Meet3. now apply Hb.
Qed.
Definition bvalid phi :=
forall (HA : CompleteHeytingAlgebra) HP, boolean HA -> Top <= hsat HP phi.
Theorem bcompleteness phi :
bvalid phi -> nil ⊢C phi.
Proof.
intros H.
specialize (H clb_calg clb_Pr (boolean_completion clb_alg_boolean)).
apply glb_calg_iff in H; eauto 2; clear H0.
- intros A psi. edestruct (nameless_equiv_all (p:=class) A psi) as (x & Hx).
exists x. now rewrite Hx.
- intros A psi chi. edestruct (nameless_equiv_ex (p:=class) A chi psi) as (x & Hx).
exists x. now rewrite Hx.
Qed.
End Lindenbaum.
From Coq Require Import Arith Lia List Program.Equality.
From Undecidability.FOL Require Import FullSyntax Heyting.Heyting Completeness.HeytingMacNeille.
Import ListNotations.
Section Lindenbaum.
Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
Context {eq_dec_Funcs : EqDec Σ_funcs}.
Context {eq_dec_Preds : EqDec Σ_preds}.
Section Completeness.
Notation "A ⊢E phi" := (A ⊢I phi) (at level 30).
Instance lb_alg : HeytingAlgebra.
Proof.
unshelve eapply (@Build_HeytingAlgebra (@form _ _ _ falsity_on)).
- intros phi psi. exact ([phi] ⊢E psi).
- exact ⊥.
- intros phi psi. exact (phi ∧ psi).
- intros phi psi. exact (phi ∨ psi).
- intros phi psi. exact (phi → psi).
- intros phi. apply Ctx. now left.
- intros phi psi theta H1 H2. apply IE with (phi:=psi); trivial.
apply Weak with (A:=[]); auto. 2: firstorder. econstructor. apply H2.
- intros phi. cbn. apply Exp, Ctx. now left.
- intros phi psi theta. cbn. split.
+ intros [H1 H2]. now apply CI.
+ intros H. split; [apply (CE1 H) | apply (CE2 H)].
- intros phi psi theta. cbn. split.
+ intros [H1 H2]. eapply DE. apply Ctx; auto. 1: now left.
eapply Weak. exact H1. firstorder.
eapply Weak. exact H2. firstorder.
+ intros H; split.
* apply (IE (phi := phi ∨ psi)). 2: try apply DI1, Ctx. 2: now left.
apply II. eapply Weak; eauto. 1: firstorder.
* apply (IE (phi := phi ∨ psi)); try apply DI2, Ctx; try now left.
apply II. eapply Weak; eauto. firstorder.
- intros phi psi theta. cbn. split.
+ intros H. apply II. apply (IE (phi := theta ∧ phi)).
* apply II. eapply Weak. 1: apply H. firstorder.
* apply CI; apply Ctx; firstorder.
+ intros H. eapply IE. 2: eapply CE2, Ctx; now left.
eapply IE. 1: eapply II, Weak. 1: apply H. 2: eapply CE1, Ctx; now left. firstorder.
Defined.
Lemma lb_alg_iff phi :
Top <= phi <-> [] ⊢E phi.
Proof.
cbn. split; intros H.
- apply (IE (phi := ¬ ⊥)); apply II; eauto using Ctx. apply Ctx. now left.
- eapply Weak; eauto; firstorder.
Qed.
Instance lb_calg : CompleteHeytingAlgebra :=
@completion_calgebra lb_alg.
Definition lb_Pr P v : lb_calg :=
embed (atom P v).
Lemma lindenbaum_hsat phi :
down phi ≡ proj1_sig (hsat lb_Pr phi).
Proof.
induction phi as [| |[]|[]] using form_ind_subst; simp hsat in *.
- rewrite down_bot. reflexivity.
- cbn. reflexivity.
- rewrite (@down_meet lb_alg f1 f2), IHphi, IHphi0. now destruct hsat, hsat.
- rewrite (@down_join lb_alg f1 f2), IHphi, IHphi0. now destruct hsat, hsat.
- rewrite (@down_impl lb_alg f1 f2), IHphi, IHphi0. now destruct hsat, hsat.
- cbn. split; intros psi H'.
+ intros X [HX [t Ht]]. change (psi ∈ proj1_sig (exist normal X HX)).
eapply Ht. rewrite <- H. apply AllE, H'.
+ apply AllI. destruct (@nameless_equiv_all _ _ _ intu ([psi]) f2) as [t Ht]. apply Ht.
apply H, H'. exists (proj2_sig (hsat lb_Pr f2[t..])), t. now destruct hsat.
- cbn. split; intros psi H'.
+ intros X [XD HX]. apply XD. intros theta HT. apply (ExE H').
destruct (@nameless_equiv_ex _ _ _ intu ([psi]) f2 theta) as [t Ht]. apply Ht.
assert (exists i : term, equiv_HA (hsat lb_Pr f2[t..]) (hsat lb_Pr f2[i..])) by now eexists.
specialize (HX (hsat lb_Pr f2[t..]) H0).
apply Weak with (A:=[f2[t..]]); auto. 2: now apply ListAutomation.incl_shift.
apply HT, HX. rewrite <- H. apply Ctx. now left.
+ specialize (H' (down (∃ f2))). apply H'.
exists (@down_normal lb_alg (∃ f2)). intros X [t ?].
intros ? ?. eapply H0 in H1.
revert x H1. fold (hset_sub (proj1_sig (hsat lb_Pr f2[t..])) (down (∃ f2))).
rewrite <- H. apply down_mono. eapply ExI, Ctx; eauto. now left.
Qed.
Lemma lindenbaum_eqH phi :
eqH (embed phi) (hsat lb_Pr phi).
Proof.
unfold eqH. cbn. now rewrite <- lindenbaum_hsat.
Qed.
Lemma lb_calg_iff phi :
Top <= hsat lb_Pr phi <-> nil ⊢E phi.
Proof.
cbn. rewrite <- lindenbaum_hsat.
rewrite <- down_top, <- lb_alg_iff. split.
- apply down_inj.
- apply down_mono.
Qed.
End Completeness.
Definition hvalid phi :=
forall (HA : CompleteHeytingAlgebra) HP, Top <= hsat HP phi.
Theorem hcompleteness phi :
hvalid phi -> nil ⊢I phi.
Proof.
intros H.
specialize (H lb_calg lb_Pr).
now eapply lb_calg_iff.
Unshelve.
Qed.
Section Completeness.
Variable gprv : list form -> form -> Prop.
Notation "A ⊢ phi" := (gprv A phi) (at level 55).
Hypothesis gCtx : forall A phi, In phi A -> A ⊢ phi.
Hypothesis gIE : forall A phi psi, A ⊢ (phi → psi) -> A ⊢ phi -> A ⊢ psi.
Hypothesis gII : forall A phi psi, (phi::A) ⊢ psi -> A ⊢ (phi → psi).
Hypothesis gExp : forall A phi, A ⊢ ⊥ -> A ⊢ phi.
Hypothesis gCI : forall A phi psi, A ⊢ phi -> A ⊢ psi -> A ⊢ (phi ∧ psi).
Hypothesis gCE1 : forall A phi psi, A ⊢ (phi ∧ psi) -> A ⊢ phi.
Hypothesis gCE2 : forall A phi psi, A ⊢ (phi ∧ psi) -> A ⊢ psi.
Hypothesis gDI1 : forall A phi psi, A ⊢ phi -> A ⊢ (phi ∨ psi).
Hypothesis gDI2 : forall A phi psi, A ⊢ psi -> A ⊢ (phi ∨ psi).
Hypothesis gDE : forall A phi psi theta, A ⊢ (phi ∨ psi) -> (phi :: A) ⊢ theta -> (psi :: A) ⊢ theta -> A ⊢ theta.
Hypothesis gWeak : forall A B phi, A ⊢ phi -> incl A B -> B ⊢ phi.
Instance glb_alg : HeytingAlgebra.
Proof.
unshelve eapply (@Build_HeytingAlgebra (form)).
- intros phi psi. exact ([phi] ⊢ psi).
- exact ⊥.
- intros phi psi. exact (phi ∧ psi).
- intros phi psi. exact (phi ∨ psi).
- intros phi psi. exact (phi → psi).
- intros phi. apply gCtx. now left.
- intros phi psi theta H1 H2. apply gIE with (phi:=psi); trivial.
apply gWeak with (A:=[]); auto. firstorder.
- intros phi. cbn. apply gExp, gCtx. now left.
- intros phi psi theta. cbn. split.
+ intros [H1 H2]. now apply gCI.
+ intros H. split; [apply (gCE1 H) | apply (gCE2 H)].
- intros phi psi theta. cbn. split.
+ intros [H1 H2]. eapply gDE. apply gCtx; auto. 1: now left.
eapply gWeak. exact H1. firstorder.
eapply gWeak. exact H2. firstorder.
+ intros H; split.
* apply (gIE (phi := phi ∨ psi)); try apply gDI1, gCtx.
apply gII. eapply gWeak; eauto. 1: firstorder. now left.
* apply (gIE (phi := phi ∨ psi)); try apply gDI2, gCtx.
apply gII. eapply gWeak; eauto. 1: firstorder. now left.
- intros phi psi theta. cbn. split.
+ intros H. apply gII. apply (gIE (phi := theta ∧ phi)).
* apply gII. eapply gWeak; eauto. firstorder.
* apply gCI; apply gCtx; auto. 1: right; now left. now left.
+ intros H. apply (gIE (phi:=phi)). 2: eapply gCE2, gCtx; now left.
eapply gIE. 1: eapply gII, gWeak. 1: apply H. 2: eapply gCE1, gCtx; now left.
firstorder.
Defined.
Lemma glb_alg_iff phi :
Top <= phi <-> [] ⊢ phi.
Proof.
cbn. split; intros H.
- apply (gIE (phi := ¬ ⊥)); apply gII. 2: apply gCtx; now left. apply H.
- eapply gWeak; eauto. firstorder.
Qed.
Instance glb_calg : CompleteHeytingAlgebra :=
@completion_calgebra glb_alg.
Definition glb_Pr P v : glb_calg :=
embed (atom P v).
Hypothesis gAllI : forall A phi, map (subst_form ↑) A ⊢ phi -> A ⊢ (∀ phi).
Hypothesis gAllE : forall A t phi, A ⊢ (∀ phi) -> A ⊢ phi[t..].
Hypothesis gExI : forall A t phi, A ⊢ phi[t..] -> A ⊢ (∃ phi).
Hypothesis gExE : forall A phi psi, A ⊢ (∃ phi) -> (phi :: map (subst_form ↑) A) ⊢ psi[↑] -> A ⊢ psi.
Hypothesis gnameless_equiv_all' : forall A phi, exists t, A ⊢ phi[t..] <-> map (subst_form ↑) A ⊢ phi.
Hypothesis gnameless_equiv_ex' : forall A phi psi, exists t, (psi[t..] :: A) ⊢ phi <-> (psi :: map (subst_form ↑) A) ⊢ phi[↑].
Lemma glindenbaum_hsat phi :
down phi ≡ proj1_sig (hsat glb_Pr phi).
Proof.
induction phi as [| |[]phi ? psi ?|[] phi ?] using form_ind_subst; simp hsat in *.
- rewrite down_bot. reflexivity.
- cbn. reflexivity.
- rewrite (@down_meet glb_alg phi psi), IHphi, IHphi0. now destruct hsat, hsat.
- rewrite (@down_join glb_alg phi psi), IHphi, IHphi0. now destruct hsat, hsat.
- rewrite (@down_impl glb_alg phi psi), IHphi, IHphi0. now destruct hsat, hsat.
- cbn. split; intros psi H'.
+ intros X [HX [t Ht]]. change (psi ∈ proj1_sig (exist normal X HX)).
eapply Ht. rewrite <- H. apply gAllE, H'.
+ apply gAllI. destruct (@gnameless_equiv_all' ([psi]) phi) as [t <-].
apply H, H'. exists (proj2_sig (hsat glb_Pr phi[t..])), t. now destruct hsat.
- cbn. split; intros psi H'.
+ intros X [XD HX]. apply XD. intros theta HT. apply (gExE H').
destruct (@gnameless_equiv_ex' ([psi]) theta phi) as [t <-].
assert (exists i : term, equiv_HA (hsat glb_Pr phi[t..]) (hsat glb_Pr phi[i..])) by now eexists.
specialize (HX (hsat glb_Pr phi[t..]) H0).
apply gWeak with (A:=[phi[t..]]); auto.
apply HT, HX. rewrite <- H. apply gCtx. now left. apply ListAutomation.incl_shift. easy.
+ specialize (H' (down (∃ phi))). apply H'.
exists (@down_normal glb_alg (∃ phi)). intros X [t ?].
intros ? ?. eapply H0 in H1.
revert x H1. fold (hset_sub (proj1_sig (hsat glb_Pr phi[t..])) (down (∃ phi))).
rewrite <- H. apply down_mono. eapply gExI, gCtx; eauto. now left.
Qed.
Lemma glindenbaum_eqH phi :
eqH (embed phi) (hsat glb_Pr phi).
Proof.
unfold eqH. cbn. now rewrite <- glindenbaum_hsat.
Qed.
Lemma glb_calg_iff phi :
Top <= hsat glb_Pr phi <-> nil ⊢ phi.
Proof.
cbn. rewrite <- glindenbaum_hsat.
rewrite <- down_top, <- glb_alg_iff. split.
- apply down_inj.
- apply down_mono.
Qed.
End Completeness.
#[local] Hint Constructors prv : core.
Instance clb_alg : HeytingAlgebra.
Proof.
apply (@glb_alg (@prv _ _ _ class)); eauto 2.
apply Weak.
Defined.
Instance clb_calg : CompleteHeytingAlgebra.
Proof.
apply (@glb_calg (@prv _ _ _ class)); eauto 2. apply Weak.
Defined.
Definition clb_Pr P (v : Vector.t term (ar_preds P)) : clb_calg.
Proof.
apply glb_Pr with P. exact v.
Defined.
Lemma clb_alg_boolean :
boolean clb_alg.
Proof.
intros phi psi. cbn. eapply IE; try apply Pc. apply Ctx. now left.
Qed.
Lemma boolean_completion HA :
boolean HA -> boolean (@completion_calgebra HA).
Proof.
intros H. intros [X HX] [Y HY]; cbn. intros a Ha.
unfold hset_impl in Ha. apply HX.
intros b Hb. specialize (Ha (Impl b Bot)).
eapply Rtra; try apply H. apply Impl1, Hb, Ha.
intros c Hc. apply HY. intros d Hd. apply Rtra with Bot; try apply Bot1.
assert (H' : Meet (Impl b Bot) c <= Impl b Bot) by apply Meet2.
apply Impl1 in H'. eapply Rtra; try eassumption. repeat rewrite <- Meet1.
repeat split; auto. eapply Rtra; try apply Meet3. now apply Hb.
Qed.
Definition bvalid phi :=
forall (HA : CompleteHeytingAlgebra) HP, boolean HA -> Top <= hsat HP phi.
Theorem bcompleteness phi :
bvalid phi -> nil ⊢C phi.
Proof.
intros H.
specialize (H clb_calg clb_Pr (boolean_completion clb_alg_boolean)).
apply glb_calg_iff in H; eauto 2; clear H0.
- intros A psi. edestruct (nameless_equiv_all (p:=class) A psi) as (x & Hx).
exists x. now rewrite Hx.
- intros A psi chi. edestruct (nameless_equiv_ex (p:=class) A chi psi) as (x & Hx).
exists x. now rewrite Hx.
Qed.
End Lindenbaum.