Require Import PslBase.FCI.
Require Import PslBase.Base.
Require Import forms.
Require Import Coq.Sorting.Permutation.
Require Import permutationSCforK.
Require Import decidability.
Require Import toolbox.
Require Import PslBase.Base.
Require Import forms.
Require Import Coq.Sorting.Permutation.
Require Import permutationSCforK.
Require Import decidability.
Require Import toolbox.
Inductive gk3c: list form -> list form -> Prop :=
| gk3cC A B x: Var x el A -> Var x el B -> gk3c A B
| gk3cF A B: Bot el A -> gk3c A B
| gk3cIL A B s t: Imp s t el A -> gk3c A (s::B) -> gk3c (t::A) B -> gk3c A B
| gk3cIR A B s t: Imp s t el B -> gk3c (s::A) (t::B) -> gk3c A B
| gk3cAL A B s t: And s t el A -> gk3c (s::t::A) B -> gk3c A B
| gk3cAR A B s t: And s t el B -> gk3c A (s::B) -> gk3c A (t::B) -> gk3c A B
| gk3cOL A B s t: Or s t el A -> gk3c (s::A) B -> gk3c (t::A) B -> gk3c A B
| gk3cOR A B s t: Or s t el B -> gk3c A (s::t::B) -> gk3c A B
| gk3cKI A B s: (K s) el B -> gk3c (remNotK A) [s] -> gk3c A B
.
Inductive gk3ch: nat -> list form -> list form -> Prop :=
| gk3chC A B x: Var x el A -> Var x el B -> gk3ch 0 A B
| gk3chF A B: Bot el A -> gk3ch 0 A B
| gk3chIL A B s t n: Imp s t el A -> gk3ch n A (s::B) -> gk3ch n (t::A) B -> gk3ch (S n) A B
| gk3chIR A B s t n: Imp s t el B -> gk3ch n (s::A) (t::B) -> gk3ch (S n) A B
| gk3chAL A B s t n: And s t el A -> gk3ch n (s::t::A) B -> gk3ch (S n) A B
| gk3chAR A B s t n: And s t el B -> gk3ch n A (s::B) -> gk3ch n A (t::B) -> gk3ch (S n) A B
| gk3chOL A B s t n: Or s t el A -> gk3ch n (s::A) B -> gk3ch n (t::A) B -> gk3ch (S n) A B
| gk3chOR A B s t n: Or s t el B -> gk3ch n A (s::t::B) -> gk3ch (S n) A B
| gk3chKI A B s n: (K s) el B -> gk3ch n (remNotK A) [s] -> gk3ch (S n) A B
| gk3chS A B n : gk3ch n A B -> gk3ch (S n) A B
.
Local Hint Constructors gk3c gk3ch : core.
Lemma gk3h_hmon n m A B : n <= m -> gk3ch n A B -> gk3ch m A B.
Proof.
intros. induction H; auto.
Qed.
Local Hint Resolve remNotK_subset : core.
Lemma gk3_height A B: gk3c A B <-> exists n, gk3ch n A B.
Proof.
split.
- intro. induction H; firstorder eauto.
+ exists (S(Nat.max x0 x)). apply gk3chIL with s t;firstorder eauto.
apply gk3h_hmon with x0; auto; lia. apply gk3h_hmon with x; auto; lia.
+ exists (S(Nat.max x0 x)). apply gk3chAR with s t;firstorder eauto.
apply gk3h_hmon with x0; auto; lia. apply gk3h_hmon with x; auto; lia.
+ exists (S(Nat.max x0 x)). apply gk3chOL with s t;firstorder eauto.
apply gk3h_hmon with x0; auto; lia. apply gk3h_hmon with x; auto; lia.
- intro. destruct H as [nh H]. induction H; firstorder eauto.
Qed.
Corollary gk3chW n A B:
gk3ch n A B -> forall A' B', A <<= A' -> B <<= B' -> gk3ch n A' B'.
Proof.
intro H. induction H; intros; eauto.
+ apply gk3chIL with s t; auto.
+ apply gk3chIR with s t; auto.
+ apply gk3chAL with s t; auto. apply IHgk3ch; auto.
+ apply gk3chAR with s t; auto.
+ apply gk3chOL with s t; auto.
+ apply gk3chOR with s t; auto. apply IHgk3ch; auto.
Qed.
Lemma gk3cW A B:
gk3c A B -> forall A' B', A <<= A' -> B <<= B' -> gk3c A' B'.
Proof.
intros H % gk3_height A' B' HA' HB'. destruct H as [nh H]. apply gk3_height. exists nh. eauto using gk3chW.
Qed.
Local Hint Resolve gk3chW : core.
| gk3cC A B x: Var x el A -> Var x el B -> gk3c A B
| gk3cF A B: Bot el A -> gk3c A B
| gk3cIL A B s t: Imp s t el A -> gk3c A (s::B) -> gk3c (t::A) B -> gk3c A B
| gk3cIR A B s t: Imp s t el B -> gk3c (s::A) (t::B) -> gk3c A B
| gk3cAL A B s t: And s t el A -> gk3c (s::t::A) B -> gk3c A B
| gk3cAR A B s t: And s t el B -> gk3c A (s::B) -> gk3c A (t::B) -> gk3c A B
| gk3cOL A B s t: Or s t el A -> gk3c (s::A) B -> gk3c (t::A) B -> gk3c A B
| gk3cOR A B s t: Or s t el B -> gk3c A (s::t::B) -> gk3c A B
| gk3cKI A B s: (K s) el B -> gk3c (remNotK A) [s] -> gk3c A B
.
Inductive gk3ch: nat -> list form -> list form -> Prop :=
| gk3chC A B x: Var x el A -> Var x el B -> gk3ch 0 A B
| gk3chF A B: Bot el A -> gk3ch 0 A B
| gk3chIL A B s t n: Imp s t el A -> gk3ch n A (s::B) -> gk3ch n (t::A) B -> gk3ch (S n) A B
| gk3chIR A B s t n: Imp s t el B -> gk3ch n (s::A) (t::B) -> gk3ch (S n) A B
| gk3chAL A B s t n: And s t el A -> gk3ch n (s::t::A) B -> gk3ch (S n) A B
| gk3chAR A B s t n: And s t el B -> gk3ch n A (s::B) -> gk3ch n A (t::B) -> gk3ch (S n) A B
| gk3chOL A B s t n: Or s t el A -> gk3ch n (s::A) B -> gk3ch n (t::A) B -> gk3ch (S n) A B
| gk3chOR A B s t n: Or s t el B -> gk3ch n A (s::t::B) -> gk3ch (S n) A B
| gk3chKI A B s n: (K s) el B -> gk3ch n (remNotK A) [s] -> gk3ch (S n) A B
| gk3chS A B n : gk3ch n A B -> gk3ch (S n) A B
.
Local Hint Constructors gk3c gk3ch : core.
Lemma gk3h_hmon n m A B : n <= m -> gk3ch n A B -> gk3ch m A B.
Proof.
intros. induction H; auto.
Qed.
Local Hint Resolve remNotK_subset : core.
Lemma gk3_height A B: gk3c A B <-> exists n, gk3ch n A B.
Proof.
split.
- intro. induction H; firstorder eauto.
+ exists (S(Nat.max x0 x)). apply gk3chIL with s t;firstorder eauto.
apply gk3h_hmon with x0; auto; lia. apply gk3h_hmon with x; auto; lia.
+ exists (S(Nat.max x0 x)). apply gk3chAR with s t;firstorder eauto.
apply gk3h_hmon with x0; auto; lia. apply gk3h_hmon with x; auto; lia.
+ exists (S(Nat.max x0 x)). apply gk3chOL with s t;firstorder eauto.
apply gk3h_hmon with x0; auto; lia. apply gk3h_hmon with x; auto; lia.
- intro. destruct H as [nh H]. induction H; firstorder eauto.
Qed.
Corollary gk3chW n A B:
gk3ch n A B -> forall A' B', A <<= A' -> B <<= B' -> gk3ch n A' B'.
Proof.
intro H. induction H; intros; eauto.
+ apply gk3chIL with s t; auto.
+ apply gk3chIR with s t; auto.
+ apply gk3chAL with s t; auto. apply IHgk3ch; auto.
+ apply gk3chAR with s t; auto.
+ apply gk3chOL with s t; auto.
+ apply gk3chOR with s t; auto. apply IHgk3ch; auto.
Qed.
Lemma gk3cW A B:
gk3c A B -> forall A' B', A <<= A' -> B <<= B' -> gk3c A' B'.
Proof.
intros H % gk3_height A' B' HA' HB'. destruct H as [nh H]. apply gk3_height. exists nh. eauto using gk3chW.
Qed.
Local Hint Resolve gk3chW : core.
Inversion results
(* This tactic can be invoked on goals of the form Γ (n)=> A if the hypothesis H and weakening prove it *)
Ltac solveWeakC H' :=
match goal with
| [ H: (gk3ch ?n ?A ?B) |- _ ] => (match H with
| H' => apply gk3chW with A B; try (auto || firstorder eauto || eauto) end)
end.
Lemma inversionIL h s t A B: In s B -> gk3ch h ((s ⊃ t)::A) B -> gk3ch h A (B).
Proof.
revert A B.
induction h.
- intros. inversion H0; destruct H1;try congruence; eauto.
- intros. inversion H0; eauto 4.
+ destruct H2.
* inversion H2; subst s0 ; subst t0. eauto.
* apply gk3chIL with s0 t0. auto. apply IHh; auto. apply IHh; auto. solveWeakC H4.
+ apply gk3chIR with s0 t0. auto. apply IHh. auto. solveWeakC H3.
+ destruct H2; try congruence. eapply gk3chAL. eauto. apply IHh; auto. solveWeakC H3.
+ apply gk3chAR with s0 t0. auto. apply IHh. auto. solveWeakC H3. apply IHh. auto. solveWeakC H4.
+ destruct H2; try congruence. eapply gk3chOL. eauto. apply IHh; auto. solveWeakC H3. apply IHh; auto. solveWeakC H4.
+ firstorder eauto.
Qed.
Lemma inversionIL2 h s t A B: In t A -> gk3ch h ((s ⊃ t)::A) B -> gk3ch h A B.
Proof.
revert A B.
induction h.
- intros. inversion H0; destruct H1;try congruence; eauto.
- intros. inversion H0; intuition. all: eauto 3.
+ destruct H2.
* inversion H2; subst s0 ; subst t0. apply gk3chS. apply IHh; auto. solveWeakC H4.
* apply gk3chIL with s0 t0. auto. apply IHh; auto. apply IHh; auto. solveWeakC H4.
+ apply gk3chIR with s0 t0. auto. apply IHh. auto. solveWeakC H3.
+ destruct H2; try congruence. eapply gk3chAL. eauto. apply IHh; auto. solveWeakC H3.
+ apply gk3chAR with s0 t0; auto.
+ destruct H2; try congruence. eapply gk3chOL. eauto. apply IHh; auto. solveWeakC H3. apply IHh; auto. solveWeakC H4.
Qed.
Lemma inversionAL h s t A B : In s A -> In t A -> gk3ch h ((s ∧ t)::A) B -> gk3ch h (A) B.
revert A B.
induction h.
- intros. inversion H1; destruct H2;try congruence; eauto.
- intros. inversion H1; intuition; eauto 3.
+ destruct H3; try congruence. eapply gk3chIL. eauto. apply IHh; auto. apply IHh; auto. solveWeakC H5.
+ apply gk3chIR with s0 t0. auto. apply IHh; auto. solveWeakC H4.
+ destruct H3.
* inversion H3; subst s0 ; subst t0. apply gk3chS. apply IHh; auto. solveWeakC H4.
* apply gk3chAL with s0 t0. auto. apply IHh; auto. solveWeakC H4.
+ apply gk3chAR with s0 t0; auto; apply IHh; auto.
+ destruct H3; try congruence. apply gk3chOL with s0 t0; auto; apply IHh; auto. solveWeakC H4. solveWeakC H5.
Qed.
Lemma inversionOR h s t A B: s el B -> t el B -> gk3ch h (A) ((s ∨ t)::B) -> gk3ch h (A) B.
Proof.
revert A B. induction h.
- intros. inversion H1. destruct H3; auto; try congruence. eauto. eauto.
- intros. inversion H1; (eauto 3).
+ apply gk3chIL with s0 t0; auto. apply IHh; auto. solveWeakC H4.
+ destruct H3; try congruence. apply gk3chIR with s0 t0. auto. apply IHh; auto. solveWeakC H4.
+ destruct H3; try congruence. apply gk3chAR with s0 t0. auto. all: apply IHh; auto. solveWeakC H4. solveWeakC H5.
+ apply gk3chOL with s0 t0; auto.
+ destruct H3.
* inversion H3. apply gk3chS. apply IHh; auto. subst s0 t0. solveWeakC H4.
* apply gk3chOR with s0 t0. auto. apply IHh; auto. solveWeakC H4.
+ destruct H3; try congruence. apply gk3chKI with s0. auto. auto.
Qed.
Lemma inversionOL1 h s t A B: s el A -> gk3ch h ((s ∨ t)::A) (B) -> gk3ch h (A) B.
Proof.
revert A B. induction h.
- intros. inversion H0. destruct H1; auto; try congruence. eauto. destruct H1; auto; try congruence.
- intros. inversion H0; eauto 3.
+ destruct H2; try congruence. apply gk3chIL with s0 t0; auto; apply IHh. auto. solveWeakC H4.
+ apply gk3chIR with s0 t0. auto. apply IHh; auto. solveWeakC H3.
+ destruct H2; try congruence. apply gk3chAL with s0 t0; auto; apply IHh. auto. solveWeakC H3.
+ apply gk3chAR with s0 t0; auto.
+ destruct H2.
* inversion H2. apply gk3chS. apply IHh; auto. subst s0 t0. solveWeakC H3.
* apply gk3chOL with s0 t0. auto. apply IHh; auto. solveWeakC H3. apply IHh. auto. solveWeakC H4.
Qed.
Lemma inversionOL2 h s t A B: t el A -> gk3ch h ((s ∨ t)::A) (B) -> gk3ch h (A) B.
Proof.
revert A B. induction h.
- intros. inversion H0. destruct H1; auto; try congruence. eauto. destruct H1; auto; try congruence.
- intros. inversion H0; eauto 4.
+ destruct H2; try congruence. apply gk3chIL with s0 t0; auto; apply IHh. auto. solveWeakC H4.
+ apply gk3chIR with s0 t0. auto. apply IHh; auto. solveWeakC H3.
+ destruct H2; try congruence. apply gk3chAL with s0 t0; auto; apply IHh. auto. solveWeakC H3.
+ destruct H2.
* inversion H2. apply gk3chS. apply IHh; auto. subst s0 t0. solveWeakC H4.
* apply gk3chOL with s0 t0. auto. apply IHh; auto. solveWeakC H3. apply IHh. auto. solveWeakC H4.
Qed.
Proof.
revert A B.
induction h.
- intros. inversion H0; destruct H1;try congruence; eauto.
- intros. inversion H0; eauto 4.
+ destruct H2.
* inversion H2; subst s0 ; subst t0. eauto.
* apply gk3chIL with s0 t0. auto. apply IHh; auto. apply IHh; auto. solveWeakC H4.
+ apply gk3chIR with s0 t0. auto. apply IHh. auto. solveWeakC H3.
+ destruct H2; try congruence. eapply gk3chAL. eauto. apply IHh; auto. solveWeakC H3.
+ apply gk3chAR with s0 t0. auto. apply IHh. auto. solveWeakC H3. apply IHh. auto. solveWeakC H4.
+ destruct H2; try congruence. eapply gk3chOL. eauto. apply IHh; auto. solveWeakC H3. apply IHh; auto. solveWeakC H4.
+ firstorder eauto.
Qed.
Lemma inversionIL2 h s t A B: In t A -> gk3ch h ((s ⊃ t)::A) B -> gk3ch h A B.
Proof.
revert A B.
induction h.
- intros. inversion H0; destruct H1;try congruence; eauto.
- intros. inversion H0; intuition. all: eauto 3.
+ destruct H2.
* inversion H2; subst s0 ; subst t0. apply gk3chS. apply IHh; auto. solveWeakC H4.
* apply gk3chIL with s0 t0. auto. apply IHh; auto. apply IHh; auto. solveWeakC H4.
+ apply gk3chIR with s0 t0. auto. apply IHh. auto. solveWeakC H3.
+ destruct H2; try congruence. eapply gk3chAL. eauto. apply IHh; auto. solveWeakC H3.
+ apply gk3chAR with s0 t0; auto.
+ destruct H2; try congruence. eapply gk3chOL. eauto. apply IHh; auto. solveWeakC H3. apply IHh; auto. solveWeakC H4.
Qed.
Lemma inversionAL h s t A B : In s A -> In t A -> gk3ch h ((s ∧ t)::A) B -> gk3ch h (A) B.
revert A B.
induction h.
- intros. inversion H1; destruct H2;try congruence; eauto.
- intros. inversion H1; intuition; eauto 3.
+ destruct H3; try congruence. eapply gk3chIL. eauto. apply IHh; auto. apply IHh; auto. solveWeakC H5.
+ apply gk3chIR with s0 t0. auto. apply IHh; auto. solveWeakC H4.
+ destruct H3.
* inversion H3; subst s0 ; subst t0. apply gk3chS. apply IHh; auto. solveWeakC H4.
* apply gk3chAL with s0 t0. auto. apply IHh; auto. solveWeakC H4.
+ apply gk3chAR with s0 t0; auto; apply IHh; auto.
+ destruct H3; try congruence. apply gk3chOL with s0 t0; auto; apply IHh; auto. solveWeakC H4. solveWeakC H5.
Qed.
Lemma inversionOR h s t A B: s el B -> t el B -> gk3ch h (A) ((s ∨ t)::B) -> gk3ch h (A) B.
Proof.
revert A B. induction h.
- intros. inversion H1. destruct H3; auto; try congruence. eauto. eauto.
- intros. inversion H1; (eauto 3).
+ apply gk3chIL with s0 t0; auto. apply IHh; auto. solveWeakC H4.
+ destruct H3; try congruence. apply gk3chIR with s0 t0. auto. apply IHh; auto. solveWeakC H4.
+ destruct H3; try congruence. apply gk3chAR with s0 t0. auto. all: apply IHh; auto. solveWeakC H4. solveWeakC H5.
+ apply gk3chOL with s0 t0; auto.
+ destruct H3.
* inversion H3. apply gk3chS. apply IHh; auto. subst s0 t0. solveWeakC H4.
* apply gk3chOR with s0 t0. auto. apply IHh; auto. solveWeakC H4.
+ destruct H3; try congruence. apply gk3chKI with s0. auto. auto.
Qed.
Lemma inversionOL1 h s t A B: s el A -> gk3ch h ((s ∨ t)::A) (B) -> gk3ch h (A) B.
Proof.
revert A B. induction h.
- intros. inversion H0. destruct H1; auto; try congruence. eauto. destruct H1; auto; try congruence.
- intros. inversion H0; eauto 3.
+ destruct H2; try congruence. apply gk3chIL with s0 t0; auto; apply IHh. auto. solveWeakC H4.
+ apply gk3chIR with s0 t0. auto. apply IHh; auto. solveWeakC H3.
+ destruct H2; try congruence. apply gk3chAL with s0 t0; auto; apply IHh. auto. solveWeakC H3.
+ apply gk3chAR with s0 t0; auto.
+ destruct H2.
* inversion H2. apply gk3chS. apply IHh; auto. subst s0 t0. solveWeakC H3.
* apply gk3chOL with s0 t0. auto. apply IHh; auto. solveWeakC H3. apply IHh. auto. solveWeakC H4.
Qed.
Lemma inversionOL2 h s t A B: t el A -> gk3ch h ((s ∨ t)::A) (B) -> gk3ch h (A) B.
Proof.
revert A B. induction h.
- intros. inversion H0. destruct H1; auto; try congruence. eauto. destruct H1; auto; try congruence.
- intros. inversion H0; eauto 4.
+ destruct H2; try congruence. apply gk3chIL with s0 t0; auto; apply IHh. auto. solveWeakC H4.
+ apply gk3chIR with s0 t0. auto. apply IHh; auto. solveWeakC H3.
+ destruct H2; try congruence. apply gk3chAL with s0 t0; auto; apply IHh. auto. solveWeakC H3.
+ destruct H2.
* inversion H2. apply gk3chS. apply IHh; auto. subst s0 t0. solveWeakC H4.
* apply gk3chOL with s0 t0. auto. apply IHh; auto. solveWeakC H3. apply IHh. auto. solveWeakC H4.
Qed.
Lemma cutElimination:
forall m n n1 n2 Γ Δ B (P1: gk3ch n1 Γ (B::Δ) ) (P2: gk3ch n2 (B::Γ) Δ) , n1 + n2 = n -> (size B) = m -> gk3c (Γ) Δ.
Proof.
intros n m.
induction n, m using le_wf_ind.
intros n1 n2 Γ Δ B P1 P2 sb hnm.
assert (scut: forall Γ Δ S, size S < size B -> (gk3c Γ (S::Δ)) -> (gk3c (S::Γ) Δ) -> (gk3c Γ Δ)).
{
intros. apply gk3_height in H2. apply gk3_height in H3. destruct H2 as [nh2 H2], H3 as [nh3 H3]. eapply H. subst m1. eapply H1. eapply H2. eapply H3. reflexivity. lia.
}
assert (rcut: forall Γ Δ n1 n2, (gk3ch n1 Γ (B::Δ)) -> (gk3ch n2 (B::Γ) Δ) -> n1+n2 < m2 -> (gk3c Γ Δ)). {
intros. eapply H0. apply H3. apply H1. apply H2. reflexivity. subst m1. auto.
}
inversion P1.
- destruct H2.
+ eapply gk3cW. eapply gk3_height. exists n2. apply P2; firstorder eauto. auto. subst B. eauto. auto.
+ eauto.
- eauto.
- apply gk3cIL with s t; auto.
+ eapply rcut. solveWeakC H2. solveWeakC P2. lia.
+ eapply rcut. apply H3. solveWeakC P2. lia.
- destruct H1.
+ subst B.
apply scut with s; simpl;try lia.
* apply gk3_height. exists n2. apply inversionIL with s t. auto. solveWeakC P2. (* InversionIL1 *)
* apply scut with t. simpl; lia.
-- apply rcut with n n2. solveWeakC H2. solveWeakC P2. lia.
-- apply gk3_height. exists n2. apply inversionIL2 with s t. auto. solveWeakC P2. (* InversionIL2 *)
+ apply gk3cIR with s t. auto.
apply rcut with n n2. solveWeakC H2. solveWeakC P2. lia.
- apply gk3cAL with s t. auto. eapply rcut. apply H2. solveWeakC P2. lia.
- destruct H1.
+ eapply scut with (S := t). subst B; simpl; lia.
eapply rcut. solveWeakC H3. solveWeakC P2. lia.
eapply scut with (S := s). subst B; simpl; lia.
eapply rcut. solveWeakC H2. solveWeakC P2. lia.
eapply gk3_height. exists n2. apply inversionAL with s t; auto. rewrite<- H1. solveWeakC P2.
+ apply gk3cAR with s t. auto. apply rcut with n n2. solveWeakC H2. solveWeakC P2. lia.
apply rcut with n n2. solveWeakC H3. solveWeakC P2. lia.
- apply gk3cOL with s t. auto.
eapply rcut. apply H2. solveWeakC P2. lia.
eapply rcut. apply H3. solveWeakC P2. lia.
- destruct H1.
+ subst B. eapply scut with t. simpl size; lia. apply scut with s. simpl size; lia. apply gk3_height. exists n. apply inversionOR with s t; auto. solveWeakC H2.
apply gk3_height. exists n2. apply inversionOL1 with s t; auto. solveWeakC P2. apply gk3_height. exists n2. apply inversionOL2 with s t. auto. solveWeakC P2.
+ apply gk3cOR with s t. auto. apply rcut with n n2. solveWeakC H2. solveWeakC P2. lia.
- inversion P2.
+ destruct H6. destruct H1; subst B; try congruence. apply gk3cKI with s. auto. apply gk3_height. eauto.
eauto.
+ destruct H6. destruct H1; subst B; try congruence. apply gk3cKI with s. auto. apply gk3_height. eauto.
eauto.
+ destruct H1.
* destruct H6; try congruence. apply gk3cIL with s0 t; auto. apply rcut with n1 n0. solveWeakC P1. solveWeakC H7. lia. apply rcut with n1 n0. solveWeakC P1. solveWeakC H8. lia.
* eapply gk3cKI. apply H1. apply gk3_height. eauto.
+ apply gk3cIR with s0 t. auto. eapply rcut with n1 n0. solveWeakC P1. solveWeakC H7. lia.
+ destruct H1.
* destruct H6; try congruence. apply gk3cAL with s0 t. auto. apply rcut with n1 n0. solveWeakC P1. solveWeakC H7. lia.
* eapply gk3cKI. apply H1. apply gk3_height. eauto.
+ apply gk3cAR with s0 t. auto. eapply rcut with n1 n0. solveWeakC P1. solveWeakC H7. lia. eapply rcut with n1 n0. solveWeakC P1. solveWeakC H8. lia.
+ destruct H1.
* destruct H6; try congruence. apply gk3cOL with s0 t; auto. apply rcut with n1 n0. solveWeakC P1. solveWeakC H7. lia. apply rcut with n1 n0. solveWeakC P1. solveWeakC H8. lia.
* eapply gk3cKI. apply H1. apply gk3_height. eauto.
+ apply gk3cOR with s0 t. auto. eapply rcut with n1 n0. solveWeakC P1. solveWeakC H7. lia.
+
destruct H1.
* apply gk3cKI with s0. auto. subst B. simpl remNotK in H7. apply scut with s. simpl; lia. apply gk3cW with (remNotK Γ) [s]; eauto. all: apply gk3_height; eauto.
* eapply gk3cKI. apply H1. apply gk3_height. eauto.
+ eapply rcut. apply P1. eauto. lia.
- eapply rcut. apply H1. eauto. lia.
Qed.
Lemma pin A B: A ≡P B -> (forall x: form,In x A <-> In x B).
Proof.
intro. firstorder eauto. rewrite<- H. auto.
rewrite H. auto.
Qed.
Lemma gk3cA A B s: s el A -> s el B -> gk3c A B.
Proof.
revert A B. induction s as [x|s IHs t IHt|s IHs t IHt|s IHs t IHt| | ];
intros A B E F.
- apply gk3cKI with x. auto. apply IHx. apply remNotK_in_iff. auto. auto.
- apply (gk3cIL E); apply gk3cIR with (s:=s) (t:=t); auto.
- apply (gk3cAL E); apply gk3cAR with (s:=s) (t:=t); auto.
- apply (gk3cOL E); apply gk3cOR with (s:=s) (t:=t); auto.
- eauto.
- eauto.
Qed.
Lemma gk3cPerm: forall Γ Δ, gk3c Γ Δ -> forall Γ' Δ', Γ ≡P Γ' -> Δ ≡P Δ' -> gk3c Γ' Δ'.
Proof.
intros Γ Δ H. induction H; intros;auto.
- eapply gk3cC. rewrite<- H1. apply H. rewrite<- H2. auto.
- apply gk3cF. firstorder eauto 10 using pin. rewrite<- H0. auto.
- apply gk3cIL with s t. rewrite<- H2. auto.
apply IHgk3c1; auto. eauto.
- apply gk3cIR with s t; firstorder eauto. rewrite<- H2. auto.
- apply gk3cAL with s t; firstorder eauto. rewrite<- H1. auto.
- apply gk3cAR with s t; firstorder eauto. rewrite<- H3. auto.
- apply gk3cOL with s t; firstorder eauto. rewrite<- H2. auto.
- apply gk3cOR with s t; firstorder eauto. rewrite<- H2. auto.
- apply gk3cKI with s. rewrite<- H2. auto. apply IHgk3c. apply remNotK_perm. auto.
auto.
Qed.
Lemma gk3_monol Γ A: gk3c Γ A -> forall Γ', Γ <<= Γ' -> gk3c Γ' A.
Proof.
intro. induction H; eauto.
- intros Γ' S. apply gk3cIL with s t; eauto.
- intros Γ' S. apply gk3cAL with s t; firstorder eauto.
- intros Γ' S. apply gk3cOL with s t; firstorder eauto.
Qed.
Lemma gk3_monor A B: gk3c A B -> forall B', B <<= B' -> gk3c A B'.
intro. induction H; eauto.
all: intros B' S.
- firstorder eauto.
- firstorder eauto.
- apply gk3cAR with s t; auto.
- apply gk3cOR with s t; auto. apply IHgk3c. auto.
Qed.
(* Register with Permutation equivalence *)
Instance gk3_proper_perm : Proper ( (@Permutation form) ==> (@Permutation form) ==> iff) (gk3c ).
Proof.
intros x y H1 a b H2. split; firstorder eauto using gk3cPerm.
Defined.
Instance incl_proper_perm : Proper ( (@Permutation form) ==> (@Permutation form) ==> iff) (@incl form ).
Proof.
intros x y H1 a b H2. split.
- intros H3 c Hc . rewrite<- H2. apply H3. rewrite H1. auto.
- intros H3 c Hc. rewrite H2. apply H3. rewrite<- H1. auto.
Defined.
(* Register with incl *)
Instance gk3_proper_weak : Proper ( (@incl form) ==> (@incl form) ==> Basics.impl) (gk3c ).
Proof.
intros x y H1 a b H2 H3. firstorder eauto using gk3_monor, gk3_monol.
Defined.
Lemma gk3c_equi_lk A B: lk A B <-> gk3c A B.
Proof.
intros.
split.
intro. induction H. induction H.
- apply gk3cC with A; auto.
- apply gk3cF. auto.
- apply gk3cIL with A B. rewrite H3. auto. rewrite H3. apply gk3_monol with Γ; auto. rewrite<- H. auto. rewrite H3. apply gk3_monol with (B::Γ). rewrite<- H1. auto. auto.
- apply gk3cIR with A B. rewrite H2. auto. apply gk3cPerm with Γ1 ((A ⊃ B)::B::Δ); try psolve. apply gk3_monor with (Δ1); auto. intros a Ha. rewrite<- H0. auto.
- apply gk3cKI with A. rewrite H1. auto. apply gk3_monol with Γ. auto. intros a Ha. apply remNotK_in_iff. rewrite H0. apply in_app_iff. left. apply in_map_iff. exists a. split; eauto.
- apply gk3cOL with A B. rewrite H3. auto. rewrite H3. apply gk3_monol with Γ1; auto. rewrite H. auto. apply gk3_monol with Γ2. auto. rewrite H1. rewrite H3. auto.
- apply gk3cOR with A B. rewrite H1; auto. apply gk3_monor with Δ1. auto. rewrite H. rewrite H1. firstorder eauto.
- apply gk3cAL with A B. rewrite H1; auto. apply gk3_monol with Γ1. firstorder eauto. rewrite H, H1. firstorder eauto.
- apply gk3cAR with A B. rewrite H3; auto. apply gk3_monor with Δ1; auto. rewrite H, H3. firstorder eauto.
apply gk3_monor with Δ2; auto. rewrite H1, H3; firstorder eauto.
- auto.
- intro. induction H.
+ exists 0. apply lkhA with x; auto.
+ exists 0. apply lkhB. auto.
+ apply Perm_In_Iff in H. destruct IHgk3c1 as [n1 IH1], IHgk3c2 as [n2 IH2], H as [lH H]. eexists (S (Nat.max n1 n2)).
rewrite<- H. apply contraction. apply lkOIL. rewrite H. apply multiStep with n1; try lia; auto. rewrite H. apply multiStep with n2; try lia. auto.
+ apply Perm_In_Iff in H. destruct IHgk3c as [n1 IH], H as [lH H]. exists (S n1). rewrite<- H. apply contraction.
apply lkOIR. rewrite H. auto.
+ apply Perm_In_Iff in H. destruct H as [lH H], IHgk3c as [n IH]. exists (S n). rewrite<- H. apply contraction.
apply lkOAL. rewrite H. auto.
+ apply Perm_In_Iff in H. destruct IHgk3c1 as [n1 IH1], IHgk3c2 as [n2 IH2], H as [lH H]. eexists (S (Nat.max n1 n2)).
rewrite<- H. apply contraction. rewrite H. apply lkOAR. apply multiStep with n1; auto; try lia. apply multiStep with n2; auto; try lia.
+ apply Perm_In_Iff in H. destruct IHgk3c1 as [n1 IH1], IHgk3c2 as [n2 IH2], H as [lH H]. eexists (S (Nat.max n1 n2)).
rewrite<- H. apply contraction. rewrite H. apply lkOOL. apply multiStep with n1; auto; try lia. apply multiStep with n2; auto; try lia.
+ apply Perm_In_Iff in H. destruct H as [lH H], IHgk3c as [n IH]. eexists (S n). rewrite<- H. apply contraction. apply lkOOR. rewrite H. auto.
+ apply Perm_In_Iff in H. destruct H as [lH H], IHgk3c as [n IH]. eexists (S n). rewrite<- H.
rewrite unK_justKNoK. assert ((notK A ++ map K (remNotK A)) ≡P (( map K (remNotK A) ++ notK A))). psolve. rewrite H1.
apply lkOKI. auto.
Qed.
Definition context := list form.
Definition goalc := prod context context.
Instance goalc_eq_dec (gamma delta: goalc) :
dec (gamma = delta).
Proof.
unfold dec. repeat decide equality.
Qed.
forall m n n1 n2 Γ Δ B (P1: gk3ch n1 Γ (B::Δ) ) (P2: gk3ch n2 (B::Γ) Δ) , n1 + n2 = n -> (size B) = m -> gk3c (Γ) Δ.
Proof.
intros n m.
induction n, m using le_wf_ind.
intros n1 n2 Γ Δ B P1 P2 sb hnm.
assert (scut: forall Γ Δ S, size S < size B -> (gk3c Γ (S::Δ)) -> (gk3c (S::Γ) Δ) -> (gk3c Γ Δ)).
{
intros. apply gk3_height in H2. apply gk3_height in H3. destruct H2 as [nh2 H2], H3 as [nh3 H3]. eapply H. subst m1. eapply H1. eapply H2. eapply H3. reflexivity. lia.
}
assert (rcut: forall Γ Δ n1 n2, (gk3ch n1 Γ (B::Δ)) -> (gk3ch n2 (B::Γ) Δ) -> n1+n2 < m2 -> (gk3c Γ Δ)). {
intros. eapply H0. apply H3. apply H1. apply H2. reflexivity. subst m1. auto.
}
inversion P1.
- destruct H2.
+ eapply gk3cW. eapply gk3_height. exists n2. apply P2; firstorder eauto. auto. subst B. eauto. auto.
+ eauto.
- eauto.
- apply gk3cIL with s t; auto.
+ eapply rcut. solveWeakC H2. solveWeakC P2. lia.
+ eapply rcut. apply H3. solveWeakC P2. lia.
- destruct H1.
+ subst B.
apply scut with s; simpl;try lia.
* apply gk3_height. exists n2. apply inversionIL with s t. auto. solveWeakC P2. (* InversionIL1 *)
* apply scut with t. simpl; lia.
-- apply rcut with n n2. solveWeakC H2. solveWeakC P2. lia.
-- apply gk3_height. exists n2. apply inversionIL2 with s t. auto. solveWeakC P2. (* InversionIL2 *)
+ apply gk3cIR with s t. auto.
apply rcut with n n2. solveWeakC H2. solveWeakC P2. lia.
- apply gk3cAL with s t. auto. eapply rcut. apply H2. solveWeakC P2. lia.
- destruct H1.
+ eapply scut with (S := t). subst B; simpl; lia.
eapply rcut. solveWeakC H3. solveWeakC P2. lia.
eapply scut with (S := s). subst B; simpl; lia.
eapply rcut. solveWeakC H2. solveWeakC P2. lia.
eapply gk3_height. exists n2. apply inversionAL with s t; auto. rewrite<- H1. solveWeakC P2.
+ apply gk3cAR with s t. auto. apply rcut with n n2. solveWeakC H2. solveWeakC P2. lia.
apply rcut with n n2. solveWeakC H3. solveWeakC P2. lia.
- apply gk3cOL with s t. auto.
eapply rcut. apply H2. solveWeakC P2. lia.
eapply rcut. apply H3. solveWeakC P2. lia.
- destruct H1.
+ subst B. eapply scut with t. simpl size; lia. apply scut with s. simpl size; lia. apply gk3_height. exists n. apply inversionOR with s t; auto. solveWeakC H2.
apply gk3_height. exists n2. apply inversionOL1 with s t; auto. solveWeakC P2. apply gk3_height. exists n2. apply inversionOL2 with s t. auto. solveWeakC P2.
+ apply gk3cOR with s t. auto. apply rcut with n n2. solveWeakC H2. solveWeakC P2. lia.
- inversion P2.
+ destruct H6. destruct H1; subst B; try congruence. apply gk3cKI with s. auto. apply gk3_height. eauto.
eauto.
+ destruct H6. destruct H1; subst B; try congruence. apply gk3cKI with s. auto. apply gk3_height. eauto.
eauto.
+ destruct H1.
* destruct H6; try congruence. apply gk3cIL with s0 t; auto. apply rcut with n1 n0. solveWeakC P1. solveWeakC H7. lia. apply rcut with n1 n0. solveWeakC P1. solveWeakC H8. lia.
* eapply gk3cKI. apply H1. apply gk3_height. eauto.
+ apply gk3cIR with s0 t. auto. eapply rcut with n1 n0. solveWeakC P1. solveWeakC H7. lia.
+ destruct H1.
* destruct H6; try congruence. apply gk3cAL with s0 t. auto. apply rcut with n1 n0. solveWeakC P1. solveWeakC H7. lia.
* eapply gk3cKI. apply H1. apply gk3_height. eauto.
+ apply gk3cAR with s0 t. auto. eapply rcut with n1 n0. solveWeakC P1. solveWeakC H7. lia. eapply rcut with n1 n0. solveWeakC P1. solveWeakC H8. lia.
+ destruct H1.
* destruct H6; try congruence. apply gk3cOL with s0 t; auto. apply rcut with n1 n0. solveWeakC P1. solveWeakC H7. lia. apply rcut with n1 n0. solveWeakC P1. solveWeakC H8. lia.
* eapply gk3cKI. apply H1. apply gk3_height. eauto.
+ apply gk3cOR with s0 t. auto. eapply rcut with n1 n0. solveWeakC P1. solveWeakC H7. lia.
+
destruct H1.
* apply gk3cKI with s0. auto. subst B. simpl remNotK in H7. apply scut with s. simpl; lia. apply gk3cW with (remNotK Γ) [s]; eauto. all: apply gk3_height; eauto.
* eapply gk3cKI. apply H1. apply gk3_height. eauto.
+ eapply rcut. apply P1. eauto. lia.
- eapply rcut. apply H1. eauto. lia.
Qed.
Lemma pin A B: A ≡P B -> (forall x: form,In x A <-> In x B).
Proof.
intro. firstorder eauto. rewrite<- H. auto.
rewrite H. auto.
Qed.
Lemma gk3cA A B s: s el A -> s el B -> gk3c A B.
Proof.
revert A B. induction s as [x|s IHs t IHt|s IHs t IHt|s IHs t IHt| | ];
intros A B E F.
- apply gk3cKI with x. auto. apply IHx. apply remNotK_in_iff. auto. auto.
- apply (gk3cIL E); apply gk3cIR with (s:=s) (t:=t); auto.
- apply (gk3cAL E); apply gk3cAR with (s:=s) (t:=t); auto.
- apply (gk3cOL E); apply gk3cOR with (s:=s) (t:=t); auto.
- eauto.
- eauto.
Qed.
Lemma gk3cPerm: forall Γ Δ, gk3c Γ Δ -> forall Γ' Δ', Γ ≡P Γ' -> Δ ≡P Δ' -> gk3c Γ' Δ'.
Proof.
intros Γ Δ H. induction H; intros;auto.
- eapply gk3cC. rewrite<- H1. apply H. rewrite<- H2. auto.
- apply gk3cF. firstorder eauto 10 using pin. rewrite<- H0. auto.
- apply gk3cIL with s t. rewrite<- H2. auto.
apply IHgk3c1; auto. eauto.
- apply gk3cIR with s t; firstorder eauto. rewrite<- H2. auto.
- apply gk3cAL with s t; firstorder eauto. rewrite<- H1. auto.
- apply gk3cAR with s t; firstorder eauto. rewrite<- H3. auto.
- apply gk3cOL with s t; firstorder eauto. rewrite<- H2. auto.
- apply gk3cOR with s t; firstorder eauto. rewrite<- H2. auto.
- apply gk3cKI with s. rewrite<- H2. auto. apply IHgk3c. apply remNotK_perm. auto.
auto.
Qed.
Lemma gk3_monol Γ A: gk3c Γ A -> forall Γ', Γ <<= Γ' -> gk3c Γ' A.
Proof.
intro. induction H; eauto.
- intros Γ' S. apply gk3cIL with s t; eauto.
- intros Γ' S. apply gk3cAL with s t; firstorder eauto.
- intros Γ' S. apply gk3cOL with s t; firstorder eauto.
Qed.
Lemma gk3_monor A B: gk3c A B -> forall B', B <<= B' -> gk3c A B'.
intro. induction H; eauto.
all: intros B' S.
- firstorder eauto.
- firstorder eauto.
- apply gk3cAR with s t; auto.
- apply gk3cOR with s t; auto. apply IHgk3c. auto.
Qed.
(* Register with Permutation equivalence *)
Instance gk3_proper_perm : Proper ( (@Permutation form) ==> (@Permutation form) ==> iff) (gk3c ).
Proof.
intros x y H1 a b H2. split; firstorder eauto using gk3cPerm.
Defined.
Instance incl_proper_perm : Proper ( (@Permutation form) ==> (@Permutation form) ==> iff) (@incl form ).
Proof.
intros x y H1 a b H2. split.
- intros H3 c Hc . rewrite<- H2. apply H3. rewrite H1. auto.
- intros H3 c Hc. rewrite H2. apply H3. rewrite<- H1. auto.
Defined.
(* Register with incl *)
Instance gk3_proper_weak : Proper ( (@incl form) ==> (@incl form) ==> Basics.impl) (gk3c ).
Proof.
intros x y H1 a b H2 H3. firstorder eauto using gk3_monor, gk3_monol.
Defined.
Lemma gk3c_equi_lk A B: lk A B <-> gk3c A B.
Proof.
intros.
split.
intro. induction H. induction H.
- apply gk3cC with A; auto.
- apply gk3cF. auto.
- apply gk3cIL with A B. rewrite H3. auto. rewrite H3. apply gk3_monol with Γ; auto. rewrite<- H. auto. rewrite H3. apply gk3_monol with (B::Γ). rewrite<- H1. auto. auto.
- apply gk3cIR with A B. rewrite H2. auto. apply gk3cPerm with Γ1 ((A ⊃ B)::B::Δ); try psolve. apply gk3_monor with (Δ1); auto. intros a Ha. rewrite<- H0. auto.
- apply gk3cKI with A. rewrite H1. auto. apply gk3_monol with Γ. auto. intros a Ha. apply remNotK_in_iff. rewrite H0. apply in_app_iff. left. apply in_map_iff. exists a. split; eauto.
- apply gk3cOL with A B. rewrite H3. auto. rewrite H3. apply gk3_monol with Γ1; auto. rewrite H. auto. apply gk3_monol with Γ2. auto. rewrite H1. rewrite H3. auto.
- apply gk3cOR with A B. rewrite H1; auto. apply gk3_monor with Δ1. auto. rewrite H. rewrite H1. firstorder eauto.
- apply gk3cAL with A B. rewrite H1; auto. apply gk3_monol with Γ1. firstorder eauto. rewrite H, H1. firstorder eauto.
- apply gk3cAR with A B. rewrite H3; auto. apply gk3_monor with Δ1; auto. rewrite H, H3. firstorder eauto.
apply gk3_monor with Δ2; auto. rewrite H1, H3; firstorder eauto.
- auto.
- intro. induction H.
+ exists 0. apply lkhA with x; auto.
+ exists 0. apply lkhB. auto.
+ apply Perm_In_Iff in H. destruct IHgk3c1 as [n1 IH1], IHgk3c2 as [n2 IH2], H as [lH H]. eexists (S (Nat.max n1 n2)).
rewrite<- H. apply contraction. apply lkOIL. rewrite H. apply multiStep with n1; try lia; auto. rewrite H. apply multiStep with n2; try lia. auto.
+ apply Perm_In_Iff in H. destruct IHgk3c as [n1 IH], H as [lH H]. exists (S n1). rewrite<- H. apply contraction.
apply lkOIR. rewrite H. auto.
+ apply Perm_In_Iff in H. destruct H as [lH H], IHgk3c as [n IH]. exists (S n). rewrite<- H. apply contraction.
apply lkOAL. rewrite H. auto.
+ apply Perm_In_Iff in H. destruct IHgk3c1 as [n1 IH1], IHgk3c2 as [n2 IH2], H as [lH H]. eexists (S (Nat.max n1 n2)).
rewrite<- H. apply contraction. rewrite H. apply lkOAR. apply multiStep with n1; auto; try lia. apply multiStep with n2; auto; try lia.
+ apply Perm_In_Iff in H. destruct IHgk3c1 as [n1 IH1], IHgk3c2 as [n2 IH2], H as [lH H]. eexists (S (Nat.max n1 n2)).
rewrite<- H. apply contraction. rewrite H. apply lkOOL. apply multiStep with n1; auto; try lia. apply multiStep with n2; auto; try lia.
+ apply Perm_In_Iff in H. destruct H as [lH H], IHgk3c as [n IH]. eexists (S n). rewrite<- H. apply contraction. apply lkOOR. rewrite H. auto.
+ apply Perm_In_Iff in H. destruct H as [lH H], IHgk3c as [n IH]. eexists (S n). rewrite<- H.
rewrite unK_justKNoK. assert ((notK A ++ map K (remNotK A)) ≡P (( map K (remNotK A) ++ notK A))). psolve. rewrite H1.
apply lkOKI. auto.
Qed.
Definition context := list form.
Definition goalc := prod context context.
Instance goalc_eq_dec (gamma delta: goalc) :
dec (gamma = delta).
Proof.
unfold dec. repeat decide equality.
Qed.
Section Decidability_GK3c.
Variable A0 B0 : context.
Definition Uc := scl (A0 ++ B0).
Definition Uc_sfc : sf_closed Uc := @scl_closed _.
Definition Gammac := list_prod (power Uc) (power Uc).
Definition stepc (Delta : list goalc) (gamma : goalc) : Prop :=
let (A,B) := gamma in
(exists (u: form), u el A /\ (u el B \/
(match u with
| Bot => True
| Imp s t => (A, rep (s::B) Uc) el Delta /\ (rep (t::A) Uc, B) el Delta
| And s t => (rep (s::t::A) Uc, B) el Delta
| Or s t => (rep (s::A) Uc, B) el Delta /\ (rep (t::A) Uc, B) el Delta
| _ => False
end) ) )
\/
(exists u, u el B /\
match u with
| Imp s t => (rep (s::A) Uc, rep (t::B) Uc) el Delta
| And s t => (A, rep (s::B) Uc) el Delta /\ (A, rep (t::B) Uc) el Delta
| Or s t => (A, rep (s::t::B) Uc) el Delta
| K s => (rep (remNotK A) Uc, (rep [s] Uc)) el Delta
| _ => False
end).
Instance step_dec Delta gamma :
dec (stepc Delta gamma).
Proof.
destruct gamma as [A u]; simpl.
apply or_dec. apply list_exists_dec. intro . destruct x; auto 10.
apply list_exists_dec. intro x. destruct x; firstorder eauto.
Defined.
Definition stepcb (Delta : list goalc) (Gamma : goalc) := dec2bool (step_dec Delta Gamma).
Lemma stepb_reflect D γ: stepcb D γ = true <-> stepc D γ.
Proof.
split; intro.
apply Dec_reflect in H. auto.
apply Dec_reflect. auto.
Qed.
Definition Lambdac :=
(FCI.C stepcb Gammac).
Lemma lambdac_closure gamma :
gamma el Gammac -> stepcb Lambdac gamma -> gamma el Lambdac.
Proof. apply FCI.closure. Qed.
Lemma gk3c_lambdac A B :
A <<= Uc -> B <<= Uc -> gk3c A B -> (rep A Uc, rep B Uc) el Lambdac.
Proof.
intros D1 D2 D.
induction D.
- (apply lambdac_closure; [now eauto using in_prod, rep_power|]); simpl.
apply stepb_reflect. left. exists (Var x). auto using rep_in.
- (apply lambdac_closure; [now eauto using in_prod, rep_power|]); simpl.
apply stepb_reflect. left. exists Bot. auto using rep_in.
- (apply lambdac_closure; [now eauto using in_prod, rep_power|]); simpl.
apply stepb_reflect. left. exists (s ⊃ t). split; auto using rep_in. right.
+ specialize (IHD1 D1). apply D1 in H. apply Uc_sfc in H as [H1 H2].
split.
assert (I: (rep A Uc, rep (s :: B) Uc) el Lambdac) by auto.
assert (J: (rep (t :: A) Uc, rep B Uc) el Lambdac) by auto.
rewrite rep_eq with (A:=s :: rep B Uc) (B:=s :: B). auto. rewrite rep_equi; auto.
rewrite rep_eq with (A:=t :: rep A Uc) (B:=t :: A); auto.
rewrite rep_equi. auto. auto.
- (apply lambdac_closure; [now eauto using in_prod, rep_power|]); simpl.
apply stepb_reflect. right. exists (Imp s t). split; auto using rep_in.
apply D2 in H. apply Uc_sfc in H as [E1 E2].
assert (I: (rep (s :: A) Uc, rep (t :: B) Uc) el Lambdac) by auto.
rewrite rep_eq with (B:=s::A).
rewrite rep_eq with (A:=t :: rep B Uc) (B:=t :: B); auto.
+ setoid_rewrite rep_equi; auto.
+ setoid_rewrite rep_equi; auto.
- (apply lambdac_closure; [now eauto using in_prod, rep_power|]); simpl.
apply stepb_reflect. left. exists (And s t). split; auto using rep_in. right.
apply D1 in H. apply Uc_sfc in H as [E1 E2].
assert (I: (rep (s :: t :: A) Uc, rep B Uc) el Lambdac) by auto.
rewrite rep_eq with (B:=s :: t :: A); auto.
rewrite rep_equi; auto.
- (apply lambdac_closure; [now eauto using in_prod, rep_power|]); simpl. apply stepb_reflect.
right. exists (And s t). split; auto using rep_in.
apply D2 in H. apply Uc_sfc in H as [E1 E2].
assert (I: (rep A Uc, rep (s :: B) Uc) el Lambdac) by auto.
assert (J: (rep A Uc, rep (t :: B) Uc) el Lambdac) by auto.
rewrite rep_eq with (A:=s :: rep B Uc) (B:=s :: B).
rewrite rep_eq with (A:=t :: rep B Uc) (B:=t :: B); auto.
+ rewrite rep_equi; auto.
+ rewrite rep_equi; auto.
- (apply lambdac_closure; [now eauto using in_prod, rep_power|]); simpl. apply stepb_reflect.
left. exists (Or s t). split; auto using rep_in. right.
apply D1 in H. apply Uc_sfc in H as [E1 E2].
assert (I: (rep (s :: A) Uc, rep B Uc) el Lambdac) by auto.
assert (J: (rep (t :: A) Uc, rep B Uc) el Lambdac) by auto.
rewrite rep_eq with (A:=s :: rep A Uc) (B:=s :: A).
rewrite rep_eq with (A:=t :: rep A Uc) (B:=t :: A); auto.
+ rewrite rep_equi; auto.
+ rewrite rep_equi; auto.
- (apply lambdac_closure; [now eauto using in_prod, rep_power|]); simpl. apply stepb_reflect.
right. exists (Or s t). split; auto using rep_in.
apply D2 in H. apply Uc_sfc in H as [E1 E2].
assert (I: (rep A Uc, rep (s :: t :: B) Uc) el Lambdac) by auto.
rewrite rep_eq with (A:=s :: t :: rep B Uc) (B:=s :: t :: B); auto.
rewrite rep_equi; auto.
- (apply lambdac_closure; [now eauto using in_prod, rep_power|]); simpl. apply stepb_reflect.
right. exists (K s). split; auto using rep_in.
assert ((rep (remNotK (rep A Uc)) Uc = (rep (remNotK A) Uc))).
{
apply rep_eq.
split.
+ intros a Ha. apply remNotK_in_iff. apply remNotK_in_iff in Ha. apply rep_incl in Ha. auto.
+ intros a Ha. apply remNotK_in_iff. apply rep_in. auto. apply remNotK_in_iff in Ha. auto.
}
assert ((rep (remNotK A) Uc, rep [s] Uc) el Lambdac). {
apply IHD.
- intros a Ha. apply remNotK_in_iff in Ha. apply D1 in Ha. apply Uc_sfc in Ha. auto.
- intros a Ha. apply D2 in H. destruct Ha; auto. subst s. apply Uc_sfc in H. auto.
}
rewrite H0. auto.
Qed.
Lemma lambdac_ind (p : goalc -> Prop) :
(forall Delta gamma, inclp Delta p ->
gamma el Gammac -> stepc Delta gamma -> p gamma)
-> inclp Lambdac p.
Proof. intros. apply FCI.ind. intros. apply H with A; auto. apply stepb_reflect. auto. Qed.
Lemma lambdac_gk3c A B :
(A,B) el Lambdac -> gk3c A B.
Proof.
revert A B.
cut (inclp Lambdac (fun gamma => gk3c (fst gamma) (snd gamma))).
{ intros E A B. apply E. }
apply lambdac_ind. intros Delta [A B] E F G; simpl.
assert (E': forall A B, (A,B) el Delta -> gk3c A B).
{ intros A' B'. apply E. } clear E.
destruct G. destruct H. destruct H as [H1 [H2 | H3]]. eapply gk3cA; eauto.
destruct x; try firstorder eauto; try tauto; try (auto using gk3cW, rep_incl).
apply E' in H. apply E' in H0.
apply gk3cIL with x1 x2; eauto using gk3cW, rep_incl.
apply gk3cAL with x1 x2; eauto using gk3cW, rep_incl.
apply gk3cOL with x1 x2; eauto using gk3cW, rep_incl.
destruct H as [u H]. destruct H as [H1 H2]; destruct u; firstorder eauto.
apply E' in H2. apply gk3cKI with u; auto. eauto using gk3cW, rep_incl.
apply gk3cIR with u1 u2; eauto using gk3cW, rep_incl.
apply gk3cAR with u1 u2; eauto using gk3cW, rep_incl.
apply gk3cOR with u1 u2; eauto using gk3cW, rep_incl.
Qed.
Theorem gk3c_dec: dec (gk3c A0 B0).
Proof.
assert (A1: A0 <<= Uc).
{ apply scl_incl; auto. }
assert (A2: B0 <<= Uc).
{ apply scl_incl; auto. }
apply dec_prop_iff with (X:= gk3c (rep A0 Uc) (rep B0 Uc)).
- split; intros E; apply (gk3cW E), rep_equi; destruct (rep_equi A1); auto.
- decide ((rep A0 Uc, rep B0 Uc) el Lambdac) as [E|E].
+ left. apply lambdac_gk3c, E.
+ right. intros F. apply E.
apply gk3c_lambdac; auto.
apply (gk3cW F); auto; apply rep_equi; auto.
Qed.
End Decidability_GK3c.
Variable A0 B0 : context.
Definition Uc := scl (A0 ++ B0).
Definition Uc_sfc : sf_closed Uc := @scl_closed _.
Definition Gammac := list_prod (power Uc) (power Uc).
Definition stepc (Delta : list goalc) (gamma : goalc) : Prop :=
let (A,B) := gamma in
(exists (u: form), u el A /\ (u el B \/
(match u with
| Bot => True
| Imp s t => (A, rep (s::B) Uc) el Delta /\ (rep (t::A) Uc, B) el Delta
| And s t => (rep (s::t::A) Uc, B) el Delta
| Or s t => (rep (s::A) Uc, B) el Delta /\ (rep (t::A) Uc, B) el Delta
| _ => False
end) ) )
\/
(exists u, u el B /\
match u with
| Imp s t => (rep (s::A) Uc, rep (t::B) Uc) el Delta
| And s t => (A, rep (s::B) Uc) el Delta /\ (A, rep (t::B) Uc) el Delta
| Or s t => (A, rep (s::t::B) Uc) el Delta
| K s => (rep (remNotK A) Uc, (rep [s] Uc)) el Delta
| _ => False
end).
Instance step_dec Delta gamma :
dec (stepc Delta gamma).
Proof.
destruct gamma as [A u]; simpl.
apply or_dec. apply list_exists_dec. intro . destruct x; auto 10.
apply list_exists_dec. intro x. destruct x; firstorder eauto.
Defined.
Definition stepcb (Delta : list goalc) (Gamma : goalc) := dec2bool (step_dec Delta Gamma).
Lemma stepb_reflect D γ: stepcb D γ = true <-> stepc D γ.
Proof.
split; intro.
apply Dec_reflect in H. auto.
apply Dec_reflect. auto.
Qed.
Definition Lambdac :=
(FCI.C stepcb Gammac).
Lemma lambdac_closure gamma :
gamma el Gammac -> stepcb Lambdac gamma -> gamma el Lambdac.
Proof. apply FCI.closure. Qed.
Lemma gk3c_lambdac A B :
A <<= Uc -> B <<= Uc -> gk3c A B -> (rep A Uc, rep B Uc) el Lambdac.
Proof.
intros D1 D2 D.
induction D.
- (apply lambdac_closure; [now eauto using in_prod, rep_power|]); simpl.
apply stepb_reflect. left. exists (Var x). auto using rep_in.
- (apply lambdac_closure; [now eauto using in_prod, rep_power|]); simpl.
apply stepb_reflect. left. exists Bot. auto using rep_in.
- (apply lambdac_closure; [now eauto using in_prod, rep_power|]); simpl.
apply stepb_reflect. left. exists (s ⊃ t). split; auto using rep_in. right.
+ specialize (IHD1 D1). apply D1 in H. apply Uc_sfc in H as [H1 H2].
split.
assert (I: (rep A Uc, rep (s :: B) Uc) el Lambdac) by auto.
assert (J: (rep (t :: A) Uc, rep B Uc) el Lambdac) by auto.
rewrite rep_eq with (A:=s :: rep B Uc) (B:=s :: B). auto. rewrite rep_equi; auto.
rewrite rep_eq with (A:=t :: rep A Uc) (B:=t :: A); auto.
rewrite rep_equi. auto. auto.
- (apply lambdac_closure; [now eauto using in_prod, rep_power|]); simpl.
apply stepb_reflect. right. exists (Imp s t). split; auto using rep_in.
apply D2 in H. apply Uc_sfc in H as [E1 E2].
assert (I: (rep (s :: A) Uc, rep (t :: B) Uc) el Lambdac) by auto.
rewrite rep_eq with (B:=s::A).
rewrite rep_eq with (A:=t :: rep B Uc) (B:=t :: B); auto.
+ setoid_rewrite rep_equi; auto.
+ setoid_rewrite rep_equi; auto.
- (apply lambdac_closure; [now eauto using in_prod, rep_power|]); simpl.
apply stepb_reflect. left. exists (And s t). split; auto using rep_in. right.
apply D1 in H. apply Uc_sfc in H as [E1 E2].
assert (I: (rep (s :: t :: A) Uc, rep B Uc) el Lambdac) by auto.
rewrite rep_eq with (B:=s :: t :: A); auto.
rewrite rep_equi; auto.
- (apply lambdac_closure; [now eauto using in_prod, rep_power|]); simpl. apply stepb_reflect.
right. exists (And s t). split; auto using rep_in.
apply D2 in H. apply Uc_sfc in H as [E1 E2].
assert (I: (rep A Uc, rep (s :: B) Uc) el Lambdac) by auto.
assert (J: (rep A Uc, rep (t :: B) Uc) el Lambdac) by auto.
rewrite rep_eq with (A:=s :: rep B Uc) (B:=s :: B).
rewrite rep_eq with (A:=t :: rep B Uc) (B:=t :: B); auto.
+ rewrite rep_equi; auto.
+ rewrite rep_equi; auto.
- (apply lambdac_closure; [now eauto using in_prod, rep_power|]); simpl. apply stepb_reflect.
left. exists (Or s t). split; auto using rep_in. right.
apply D1 in H. apply Uc_sfc in H as [E1 E2].
assert (I: (rep (s :: A) Uc, rep B Uc) el Lambdac) by auto.
assert (J: (rep (t :: A) Uc, rep B Uc) el Lambdac) by auto.
rewrite rep_eq with (A:=s :: rep A Uc) (B:=s :: A).
rewrite rep_eq with (A:=t :: rep A Uc) (B:=t :: A); auto.
+ rewrite rep_equi; auto.
+ rewrite rep_equi; auto.
- (apply lambdac_closure; [now eauto using in_prod, rep_power|]); simpl. apply stepb_reflect.
right. exists (Or s t). split; auto using rep_in.
apply D2 in H. apply Uc_sfc in H as [E1 E2].
assert (I: (rep A Uc, rep (s :: t :: B) Uc) el Lambdac) by auto.
rewrite rep_eq with (A:=s :: t :: rep B Uc) (B:=s :: t :: B); auto.
rewrite rep_equi; auto.
- (apply lambdac_closure; [now eauto using in_prod, rep_power|]); simpl. apply stepb_reflect.
right. exists (K s). split; auto using rep_in.
assert ((rep (remNotK (rep A Uc)) Uc = (rep (remNotK A) Uc))).
{
apply rep_eq.
split.
+ intros a Ha. apply remNotK_in_iff. apply remNotK_in_iff in Ha. apply rep_incl in Ha. auto.
+ intros a Ha. apply remNotK_in_iff. apply rep_in. auto. apply remNotK_in_iff in Ha. auto.
}
assert ((rep (remNotK A) Uc, rep [s] Uc) el Lambdac). {
apply IHD.
- intros a Ha. apply remNotK_in_iff in Ha. apply D1 in Ha. apply Uc_sfc in Ha. auto.
- intros a Ha. apply D2 in H. destruct Ha; auto. subst s. apply Uc_sfc in H. auto.
}
rewrite H0. auto.
Qed.
Lemma lambdac_ind (p : goalc -> Prop) :
(forall Delta gamma, inclp Delta p ->
gamma el Gammac -> stepc Delta gamma -> p gamma)
-> inclp Lambdac p.
Proof. intros. apply FCI.ind. intros. apply H with A; auto. apply stepb_reflect. auto. Qed.
Lemma lambdac_gk3c A B :
(A,B) el Lambdac -> gk3c A B.
Proof.
revert A B.
cut (inclp Lambdac (fun gamma => gk3c (fst gamma) (snd gamma))).
{ intros E A B. apply E. }
apply lambdac_ind. intros Delta [A B] E F G; simpl.
assert (E': forall A B, (A,B) el Delta -> gk3c A B).
{ intros A' B'. apply E. } clear E.
destruct G. destruct H. destruct H as [H1 [H2 | H3]]. eapply gk3cA; eauto.
destruct x; try firstorder eauto; try tauto; try (auto using gk3cW, rep_incl).
apply E' in H. apply E' in H0.
apply gk3cIL with x1 x2; eauto using gk3cW, rep_incl.
apply gk3cAL with x1 x2; eauto using gk3cW, rep_incl.
apply gk3cOL with x1 x2; eauto using gk3cW, rep_incl.
destruct H as [u H]. destruct H as [H1 H2]; destruct u; firstorder eauto.
apply E' in H2. apply gk3cKI with u; auto. eauto using gk3cW, rep_incl.
apply gk3cIR with u1 u2; eauto using gk3cW, rep_incl.
apply gk3cAR with u1 u2; eauto using gk3cW, rep_incl.
apply gk3cOR with u1 u2; eauto using gk3cW, rep_incl.
Qed.
Theorem gk3c_dec: dec (gk3c A0 B0).
Proof.
assert (A1: A0 <<= Uc).
{ apply scl_incl; auto. }
assert (A2: B0 <<= Uc).
{ apply scl_incl; auto. }
apply dec_prop_iff with (X:= gk3c (rep A0 Uc) (rep B0 Uc)).
- split; intros E; apply (gk3cW E), rep_equi; destruct (rep_equi A1); auto.
- decide ((rep A0 Uc, rep B0 Uc) el Lambdac) as [E|E].
+ left. apply lambdac_gk3c, E.
+ right. intros F. apply E.
apply gk3c_lambdac; auto.
apply (gk3cW F); auto; apply rep_equi; auto.
Qed.
End Decidability_GK3c.