ICL.PropL
Definition var := nat.
Inductive form : Type :=
| Var : var -> form
| Imp : form -> form -> form
| Fal : form.
Definition Not s := Imp s Fal.
Instance form_eq_dec : forall s t:form, dec (s = t).
Proof. unfold dec. repeat decide equality. Qed.
Fixpoint vars (s : form) : list var :=
match s with
| Var x => [x]
| Imp s t => vars s ++ vars t
| Fal => nil
end.
Definition assn := var -> bool.
Fixpoint satis (f : assn) (s : form) : Prop :=
match s with
| Var x => f x = true
| Imp s1 s2 => satis f s1 -> satis f s2
| Fal => False
end.
Instance satis_dec : forall f s, dec (satis f s).
Proof.
intros f s. induction s as [x|s IHs t IHt|]; simpl; auto.
Qed.
Section F.
Variable F:Type.
(*** E is an entailment relation ***)
Variable E:list F -> F -> Prop.
(*** Structural Properties ***)
Definition Monotonicity : Prop :=
forall A A' s, A <<= A' -> E A s -> E A' s.
Definition Reflexivity : Prop :=
forall A s, s el A -> E A s.
Definition Cut : Prop :=
forall A s t, E A s -> E (s::A) t -> E A t.
Definition Consistency : Prop :=
exists s:F, ~E nil s.
End F.
Fixpoint andlist (A:list Prop) : Prop :=
match A with
| P::A' => P /\ andlist A'
| nil => True
end.
Lemma andlistEq (A:list Prop) : andlist A <-> forall s, s el A -> s.
Proof.
induction A; simpl; try tauto. split.
- intros [B C] s [D|D]; try congruence. now apply IHA.
- intros B. split.
+ apply B. tauto.
+ apply IHA. intros s C. apply B. tauto.
Qed.
Goal
let E : list Prop -> Prop -> Prop := fun A s => andlist A -> s in
Reflexivity E /\ Monotonicity E /\ Cut E /\ Consistency E.
Proof.
intros E. repeat split.
- intros A s B C. revert s B. now apply andlistEq.
- intros A A' s B C D. apply C. apply andlistEq. intros t G. apply B in G. revert t G.
now apply andlistEq.
- intros A s t B C D. apply C. split; try assumption. now apply B.
- exists False. unfold E. simpl. tauto.
Qed.
(*** Entailment Relations for form ***)
Definition context := list form.
(*** Logical Properties ***)
Definition CharImp (E:context -> form -> Prop) : Prop :=
forall A s t, E A (Imp s t) <-> E (s::A) t.
Definition CharFal (E:context -> form -> Prop) : Prop :=
forall A, E A Fal <-> forall s, E A s.
Definition bsc A s : Prop := forall f, (forall u, u el A -> satis f u) -> satis f s.
Fixpoint subst (sigma : var -> form) (s : form) : form :=
match s with
| Var x => sigma x
| Imp s t => Imp (subst sigma s) (subst sigma t)
| Fal => Fal
end.
Definition Substitution (E:context -> form -> Prop) :=
forall A s sigma, E A s -> E (map (subst sigma) A) (subst sigma s).
Definition EntailRelAllProps (E:context -> form -> Prop) :=
Reflexivity E /\ Monotonicity E /\ Cut E /\ Consistency E
/\ CharImp E /\ CharFal E /\ Substitution E.
Variable F:Type.
(*** E is an entailment relation ***)
Variable E:list F -> F -> Prop.
(*** Structural Properties ***)
Definition Monotonicity : Prop :=
forall A A' s, A <<= A' -> E A s -> E A' s.
Definition Reflexivity : Prop :=
forall A s, s el A -> E A s.
Definition Cut : Prop :=
forall A s t, E A s -> E (s::A) t -> E A t.
Definition Consistency : Prop :=
exists s:F, ~E nil s.
End F.
Fixpoint andlist (A:list Prop) : Prop :=
match A with
| P::A' => P /\ andlist A'
| nil => True
end.
Lemma andlistEq (A:list Prop) : andlist A <-> forall s, s el A -> s.
Proof.
induction A; simpl; try tauto. split.
- intros [B C] s [D|D]; try congruence. now apply IHA.
- intros B. split.
+ apply B. tauto.
+ apply IHA. intros s C. apply B. tauto.
Qed.
Goal
let E : list Prop -> Prop -> Prop := fun A s => andlist A -> s in
Reflexivity E /\ Monotonicity E /\ Cut E /\ Consistency E.
Proof.
intros E. repeat split.
- intros A s B C. revert s B. now apply andlistEq.
- intros A A' s B C D. apply C. apply andlistEq. intros t G. apply B in G. revert t G.
now apply andlistEq.
- intros A s t B C D. apply C. split; try assumption. now apply B.
- exists False. unfold E. simpl. tauto.
Qed.
(*** Entailment Relations for form ***)
Definition context := list form.
(*** Logical Properties ***)
Definition CharImp (E:context -> form -> Prop) : Prop :=
forall A s t, E A (Imp s t) <-> E (s::A) t.
Definition CharFal (E:context -> form -> Prop) : Prop :=
forall A, E A Fal <-> forall s, E A s.
Definition bsc A s : Prop := forall f, (forall u, u el A -> satis f u) -> satis f s.
Fixpoint subst (sigma : var -> form) (s : form) : form :=
match s with
| Var x => sigma x
| Imp s t => Imp (subst sigma s) (subst sigma t)
| Fal => Fal
end.
Definition Substitution (E:context -> form -> Prop) :=
forall A s sigma, E A s -> E (map (subst sigma) A) (subst sigma s).
Definition EntailRelAllProps (E:context -> form -> Prop) :=
Reflexivity E /\ Monotonicity E /\ Cut E /\ Consistency E
/\ CharImp E /\ CharFal E /\ Substitution E.
Inductive nd : context -> form -> Prop :=
| ndA A s : s el A -> nd A s
| ndII A s t : nd (s::A) t -> nd A (Imp s t)
| ndIE A s t : nd A (Imp s t) -> nd A s -> nd A t
| ndE A s : nd A Fal -> nd A s.
Goal forall A s t, nd A (Imp s (Imp (Not s) t)).
Proof.
intros A s t. apply ndII, ndII. apply ndE. apply ndIE with (s := s).
- apply ndA. left. reflexivity.
- apply ndA. right. left. reflexivity.
Qed.
Goal forall A s t, nd A (Imp s (Imp (Not s) t)).
Proof.
intros A s t.
assert (B:Not s el Not s::s::A) by auto.
assert (C:s el Not s::s::A) by auto.
exact (ndII (ndII (ndE t (ndIE (ndA B) (ndA C))))).
Qed.
Lemma ndapp A s u :
Imp s u el A -> nd A s -> nd A u.
Proof.
intros E F. apply ndIE with (s := s).
- apply ndA, E.
- exact F.
Qed.
Lemma ndapp1 A s u :
nd (Imp s u :: A) s -> nd (Imp s u :: A) u.
Proof. apply ndapp. auto. Qed.
Lemma ndapp2 A s t u :
nd (t :: Imp s u :: A) s -> nd (t :: Imp s u :: A) u.
Proof. apply ndapp. auto. Qed.
Lemma ndapp3 A s t u v :
nd (t :: v :: Imp s u :: A) s -> nd (t :: v :: Imp s u :: A) u.
Proof. apply ndapp. auto. Qed.
Lemma nd_weak A A' s :
A <<= A' -> nd A s -> nd A' s.
Proof.
intros E F. revert A' E.
induction F as [A s F|A s t F IHF|A s t F1 IHF1 F2 IHF2|A s F IHF] ; intros A' E.
- apply ndA, E. assumption.
- apply ndII, IHF. apply incl_shift, E.
- apply ndIE with (s:=s) ; auto.
- apply ndE, IHF, E.
Qed.
Lemma ndW A s t :
nd A s -> nd (t::A) s.
Proof. apply nd_weak; auto. Qed.
Lemma ndIE_weak A B s t :
nd B (Imp s t) -> B <<= A -> nd A s -> nd A t.
Proof.
intros E F G. apply ndIE with (s:=s).
- exact (nd_weak F E).
- exact G.
Qed.
Lemma ndDN A s :
nd A s -> nd A (Not (Not s)).
Proof. intros E. apply ndII, ndapp1, ndW, E. Qed.
Lemma nd_bool_sound A s :
nd A s -> bsc A s.
Proof.
intros B f.
induction B as [A s B|A s t B IHB|A s t B1 IHB1 B2 IHB2|A s B IHB]; simpl in *|-*; auto; try tauto.
intros C D. apply IHB. intros u [E|E]; auto. congruence.
Qed.
Lemma nd_con : ~ nd nil Fal.
Proof.
intros B. change (satis (fun _ => false) Fal). apply (nd_bool_sound B); simpl; tauto.
Qed.
Lemma nd_subst A s sigma : nd A s -> nd (map (subst sigma) A) (subst sigma s).
Proof.
intros B. induction B as [A s B|A s t B IHB|A s t B1 IHB1 B2 IHB2|A s B IHB].
- apply ndA. apply in_map_iff. eauto.
- simpl. apply ndII. exact IHB.
- apply ndIE with (s := subst sigma s); tauto.
- apply ndE. exact IHB.
Qed.
Inductive ndc : context -> form -> Prop :=
| ndcA A s : s el A -> ndc A s
| ndcII A s t : ndc (s::A) t -> ndc A (Imp s t)
| ndcIE A s t : ndc A (Imp s t) -> ndc A s -> ndc A t
| ndcC A s : ndc (Not s :: A) Fal -> ndc A s.
Lemma ndc_weak A A' s :
A <<= A' -> ndc A s -> ndc A' s.
Proof.
intros E F. revert A' E.
induction F as [A s F|A s t F IHF|A s t F1 IHF1 F2 IHF2|A s F IHF] ; intros A' E.
- apply ndcA, E. assumption.
- apply ndcII, IHF. apply incl_shift, E.
- apply ndcIE with (s:=s) ; auto.
- apply ndcC, IHF. intros t [G|G].
+ rewrite G. left. reflexivity.
+ right. apply E. exact G.
Qed.
Lemma ndcW A s t :
ndc A s -> ndc (t::A) s.
Proof. apply ndc_weak; auto. Qed.
Lemma ndcE A s :
ndc A Fal -> ndc A s.
Proof. intros E. apply ndcC, ndcW, E. Qed.
Lemma nd_ndc A s :
nd A s -> ndc A s.
Proof.
intros F ; induction F as [A s F|A s t F IHF|A s t F1 IHF1 F2 IHF2|A s F IHF].
- apply ndcA. assumption.
- apply ndcII, IHF.
- apply ndcIE with (s:=s) ; auto.
- apply ndcE, IHF.
Qed.
Lemma ndc_refute A s :
ndc A s <-> ndc (Not s :: A) Fal.
Proof.
split ; intros E.
- apply ndcIE with (s:=s).
+ apply ndcA. auto.
+ apply ndcW, E.
- apply ndcC, E.
Qed.
Lemma ndcapp A s u :
Imp s u el A -> ndc A s -> ndc A u.
Proof.
intros E F. apply ndcIE with (s := s).
- apply ndcA, E.
- exact F.
Qed.
Lemma ndcapp1 A s u :
ndc (Imp s u :: A) s -> ndc (Imp s u :: A) u.
Proof. apply ndcapp. auto. Qed.
Lemma ndcapp2 A s t u :
ndc (t :: Imp s u :: A) s -> ndc (t :: Imp s u :: A) u.
Proof. apply ndcapp. auto. Qed.
Lemma ndcapp3 A s t u v :
ndc (t :: v :: Imp s u :: A) s -> ndc (t :: v :: Imp s u :: A) u.
Proof. apply ndcapp. auto. Qed.
(*** Exercise ***)
Goal forall A s, ndc A (Imp (Not (Not s)) s).
Proof.
intros A s. apply ndcII, ndcC. apply ndcIE with (s:= Not s).
- apply ndcW, ndcA. auto.
- apply ndcA. auto.
Qed.
Glivenko's theorem
Lemma Glivenko A s :
ndc A s -> nd A (Not (Not s)).
Proof.
intros E. induction E as [A s E|A s t E IHE|A s t E1 IHE1 E2 IHE2|A s E IHE].
- apply ndDN, ndA. assumption.
- apply ndII, ndapp1.
apply ndII, ndE. apply (ndIE_weak IHE).
+ auto.
+ apply ndII. apply ndapp3. apply ndII. apply ndA. auto.
- apply ndII. apply (ndIE_weak IHE2).
+ auto.
+ apply ndII. apply (ndIE_weak IHE1).
* auto.
* apply ndII. apply ndapp3. apply ndapp1. apply ndA. auto.
- apply ndII. apply (ndIE IHE). apply ndII, ndA. auto.
Qed.
Corollary Glivenko_refute A :
nd A Fal <-> ndc A Fal.
Proof.
split.
- apply nd_ndc.
- intros E. apply Glivenko in E. apply (ndIE E). apply ndII, ndA. auto.
Qed.
Corollary nd_embeds_ndc A s :
ndc A s <-> nd (Not s :: A) Fal.
Proof. setoid_rewrite ndc_refute. symmetry. apply Glivenko_refute. Qed.
Intuitionistic Hilbert system
Definition FK (s t : form) : form :=
Imp s (Imp t s).
Definition FS (s t u : form) : form :=
(Imp (Imp s (Imp t u))
(Imp (Imp s t)
(Imp s u))).
Inductive hil (A : context) : form -> Prop :=
| hilA s : s el A -> hil A s
| hilK s t : hil A (FK s t)
| hilS s t u : hil A (FS s t u)
| hilE s : hil A (Imp Fal s)
| hilMP s t : hil A (Imp s t) -> hil A s -> hil A t.
Lemma hil_nd A s :
hil A s -> nd A s.
Proof.
intros E. induction E as [s E|s t|s t u|s|s t E1 IHE1 E2 IHE2].
- apply ndA. assumption.
- apply ndII, ndII, ndA. auto.
- apply ndII, ndII, ndII.
apply ndIE with (s:= Imp t u).
+ apply ndII. apply ndapp1. apply ndapp3. apply ndA. auto.
+ apply ndapp3, ndA. auto.
- apply ndII. apply ndE, ndA. auto.
- exact (ndIE IHE1 IHE2).
Qed.
Lemma hilAK A s t :
hil A s -> hil A (Imp t s).
Proof. apply hilMP. apply hilK. Qed.
Lemma hilAS A s t u :
hil A (Imp s (Imp t u)) -> hil A (Imp s t) -> hil A (Imp s u).
Proof. intros B. apply hilMP. revert B. apply hilMP. apply hilS. Qed.
Lemma hilI A s :
hil A (Imp s s).
Proof.
assert (E:= hilS A s (Imp s s) s).
assert (F:= hilK A s (Imp s s)).
assert (G:= hilK A s s).
unfold FS, FK in *.
exact (hilMP (hilMP E F) G).
Qed.
Lemma hilD s A t :
hil (s::A) t -> hil A (Imp s t).
Proof.
intros E. induction E as [t E|t u|t u v|t|t u E1 IHE1 E2 IHE2].
- destruct E as [E|E].
+ subst t. apply hilI.
+ apply hilAK. apply hilA, E.
- apply hilAK, hilK.
- apply hilAK, hilS.
- apply hilAK, hilE.
- apply hilAS with (t:=t) ; assumption.
Qed.
Lemma nd_hil A s :
nd A s -> hil A s.
Proof.
intros E. induction E as [A s E|A s t E IHE|A s t E1 IHE1 E2 IHE2|A s E IHE].
- apply hilA. assumption.
- apply hilD, IHE.
- exact (hilMP IHE1 IHE2).
- exact (hilMP (hilE A s) IHE).
Qed.
Theorem hil_iff_nd A s :
hil A s <-> nd A s.
Proof. split. apply hil_nd. apply nd_hil. Qed.