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.

# Case study: The classical modal logic K

## Sequent Calculus for K

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.

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.

## Inversion Results for K

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.

## Cut-Elimination for K

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.

## Decidability for K

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.