ICL.Gentzen
Require Export PropL.
Inductive gen : context -> form -> Prop :=
| genV A x : Var x el A -> gen A (Var x)
| genF A u : Fal el A -> gen A u
| genIR A s t : gen (s::A) t -> gen A (Imp s t)
| genIL A s t u : Imp s t el A -> gen A s -> gen (t::A) u -> gen A u.
Lemma gen_nd A s :
gen A s -> nd A s.
Proof.
induction 1; eauto using nd.
Qed.
Inductive gen : context -> form -> Prop :=
| genV A x : Var x el A -> gen A (Var x)
| genF A u : Fal el A -> gen A u
| genIR A s t : gen (s::A) t -> gen A (Imp s t)
| genIL A s t u : Imp s t el A -> gen A s -> gen (t::A) u -> gen A u.
Lemma gen_nd A s :
gen A s -> nd A s.
Proof.
induction 1; eauto using nd.
Qed.
Consistency
Unprovability of DN
Lemma gen_DN' A x s :
A <<= [Var x; Not (Not (Var x))] -> gen A s -> s <> Fal /\ s <> Not (Var x).
Proof.
intros H D.
induction D as [A y E|A v E|A s t E IHE|A s t v E F IHF G _ ].
- split; discriminate.
- exfalso. apply H in E. unfold In in E; intuition; discriminate.
- split; intros J; inv J. cut (Fal <> Fal). now auto. apply IHE; auto.
- exfalso. apply H in E. destruct E as [E|[E|[]]]; inv E. apply IHF; auto.
Qed.
Lemma gen_DN x :
~ gen [Not (Not (Var x))] (Var x).
Proof.
intros E.
inv E; unfold In in *; intuition; try discriminate.
inv H2. apply gen_DN' with (x:=x) in H0; intuition.
Qed.
Assumption rule
Weakening rule
Lemma genW A B s :
gen A s -> A <<= B -> gen B s.
Proof.
intros C; revert B.
induction C; eauto 7 using gen.
Qed.
Cut rule
Lemma genC' A s B u :
gen A s -> gen B u -> gen (A ++ rem B s) u.
Proof with auto.
intro C; revert A C B u.
induction s as [x|s IHs t IHt|]; intros A C.
- remember (Var x) as v.
induction C as [A y E|A v E| |A s t v E F _ _ IHG];
intros B u D; subst; try inv Heqv.
+ apply (genW D)...
+ apply genF...
+ eapply genIL; eauto. apply (genW F)...
- remember (Imp s t) as v.
induction C as [ |A v E|A s' t' E _|A s' t' v E F _ _ IHG];
intros B u D; subst; try inv Heqv.
+ apply genF...
+ induction D as [B y F|B u F|B s' t' F IHF|B s' t' u F G IHG H IHH].
* apply genV. assert (Var y <> Imp s t) by congruence...
* apply genF. assert (Fal <> Imp s t) by congruence...
* apply genIR. apply (genW IHF)...
* { decide (Imp s' t' = Imp s t) as [K|K].
- inv K. (* Imp s t is principal formula of both derivations *)
specialize (IHs _ IHG _ _ E).
specialize (IHt _ IHs _ _ IHH).
apply (genW IHt).
repeat apply incl_app...
apply rem_app'...
rewrite rem_comm...
- clear IHs IHt. eapply genIL; eauto. apply (genW IHH)... }
+ eapply genIL; eauto. apply (genW F)...
- remember Fal as v.
induction C as [ |A v E| |A s t v E F _ _ IHG];
intros B u D; subst; try inv Heqv.
+ apply (genW D)...
+ eapply genIL; eauto. apply (genW F)...
Qed.
Lemma genC A s u :
gen A s -> gen (s::A) u -> gen A u.
Proof.
intros E F. apply (genW (genC' E F)). auto.
Qed.
Completeness for ND
Lemma nd_gen A s :
nd A s -> gen A s.
Proof.
intros D.
induction D as [A s D|A s t _ IHD|A s t _ IHD _ IHC|A s _ IHD].
- apply genA, D.
- apply genIR, IHD.
- apply (genC IHD). eapply genIL; eauto using genA.
apply (genW IHC). auto.
- apply (genC IHD). apply genF; auto.
Qed.
Theorem gen_iff_nd A s :
gen A s <-> nd A s.
Proof.
split. apply gen_nd. apply nd_gen.
Qed.
Subformula Closure
Definition sf_closed (A : context) : Prop :=
forall u, u el A -> match u with
| Imp s t => s el A /\ t el A
| _ => True
end.
Lemma sf_closed_app A B :
sf_closed A -> sf_closed B -> sf_closed (A ++ B).
Proof.
intros E F [|s t|] G; auto.
apply in_app_or in G as [G|G].
- apply E in G. intuition; eauto.
- apply F in G. intuition; eauto.
Qed.
Lemma sf_closed_cons s t A :
s el A -> t el A -> sf_closed A -> sf_closed (Imp s t :: A).
Proof.
intros D E F [|s' t'|] G; auto.
destruct G as [G|G].
- inv G. auto.
- apply (F _) in G. destruct G; auto.
Qed.
Fixpoint scl' (s : form) : context :=
s :: match s with
| Imp u v => scl' u ++ scl' v
| _ => nil
end.
Lemma scl'_in s :
s el scl' s.
Proof.
destruct s; simpl; auto.
Qed.
Lemma scl'_closed s :
sf_closed (scl' s).
Proof.
induction s; simpl; auto.
- intros u [A|A]; inv A; auto.
- apply sf_closed_cons; auto using scl'_in, sf_closed_app.
- intros u [A|A]; inv A; auto.
Qed.
Fixpoint scl (A : context) : context :=
match A with
| nil => nil
| s :: A' => scl' s ++ scl A'
end.
Lemma scl_incl' A :
A <<= scl A.
Proof.
induction A as [|s A]; simpl; auto using scl'_in.
Qed.
Lemma scl_incl A B :
A <<= B -> A <<= scl B.
Proof.
intros E. setoid_rewrite E. apply scl_incl'.
Qed.
Lemma scl_closed A :
sf_closed (scl A).
Proof.
induction A as [|s A]; simpl. now auto.
auto using scl'_closed, sf_closed_app.
Qed.
Decidability
Definition goal := prod (context) form.
Instance goal_eq_dec gamma delta :
dec (gamma = delta :> goal).
Proof.
unfold dec. repeat decide equality.
Qed.
Section Decidability.
Variable A0 : context.
Variable s0 : form.
Definition U := scl (s0::A0).
Definition U_sfc : sf_closed U := @scl_closed _.
Definition Gamma := list_prod (power U) U.
Definition step (Delta : list goal) (gamma : goal) : Prop :=
let (A,u) := gamma in
match u with
| Var _ => u el A
| Imp s t => (rep (s::A) U, t) el Delta
| _ => False
end
\/
exists v, v el A /\
match v with
| Fal => True
| Imp s t => (A, s) el Delta /\ (rep (t::A) U, u) el Delta
| _ => False
end.
Instance step_dec Delta gamma :
dec (step Delta gamma).
Proof.
destruct gamma as [A u]; simpl.
apply or_dec.
- destruct u as [x|s t|]; auto.
- apply list_exists_dec. intros [x|s t|]; auto.
Qed.
Definition Lambda : list goal :=
FCI.C (step := step) Gamma.
Lemma lambda_closure gamma :
gamma el Gamma -> step Lambda gamma -> gamma el Lambda.
Proof. apply FCI.closure. Qed.
Lemma lambda_ind (p : goal -> Prop) :
(forall Delta gamma, inclp Delta p -> gamma el Gamma -> step Delta gamma -> p gamma) -> inclp Lambda p.
Proof. apply FCI.ind. Qed.
Lemma gen_lambda A u :
A <<= U -> u el U -> gen A u -> (rep A U,u) el Lambda.
Proof.
intros D1 D2 E.
induction E as [A x F|A u F|A s t F IHF|A s t u F G IHG H IHH];
(apply lambda_closure; [now eauto using in_prod, rep_power|]); simpl.
-left. auto using rep_in.
- right. exists Fal. auto using rep_in.
- apply U_sfc in D2 as [D2 D3].
left. rewrite rep_eq with (B := s::A).
+ auto.
+ setoid_rewrite rep_equi; auto.
- assert (K := F). apply D1 in K.
apply U_sfc in K as [K1 K2].
right. exists (Imp s t); repeat split; auto using rep_in.
rewrite rep_eq with (B := t::A).
+ auto.
+ setoid_rewrite rep_equi; auto.
Qed.
Lemma lambda_gen A u :
(A,u) el Lambda -> gen A u.
Proof.
revert A u.
cut (inclp Lambda (fun gamma => gen (fst gamma) (snd gamma))).
{ intros E A u. apply E. }
apply lambda_ind. intros Delta [A u] E F G; simpl.
assert (E': forall B v, (B,v) el Delta -> gen B v).
{ intros B v. apply E. }
clear E.
destruct G as [G|[[x|s t|] [G H]]].
- destruct u; intuition; eauto using gen, genW, rep_incl.
- contradiction H.
- intuition; eauto using gen, genW, rep_incl.
- eauto using gen.
Qed.
Theorem nd_dec :
dec (nd A0 s0).
Proof.
apply (dec_prop_iff (gen_iff_nd _ _)).
assert (A1: A0 <<= U).
{ apply scl_incl; auto. }
assert (A2: s0 el U).
{ apply scl_incl'; auto. }
apply dec_prop_iff with (X:= gen (rep A0 U) s0).
- split; intros E; apply (genW E), rep_equi; auto.
- decide ((rep A0 U, s0) el Lambda) as [E|E].
+ left. apply lambda_gen, E.
+ right. intros F. apply E.
apply gen_lambda; auto.
apply genW with (A := rep A0 U); auto.
apply rep_equi, A1.
Qed.
End Decidability.