Ltac.ipynb

prop.v

Print list.

Fixpoint In {A} (a:A) (l:list A) : Prop :=
  match l with
    | nil => False
    | cons b m => b = a \/ In a m
  end.

Print nil.

Print or.
Print eq.

Context {atom : Type}.

Inductive prop1 : Type :=
  | atom_prop1 : atom -> prop1.

Print prop1.
Check atom.
Print atom.

Inductive SC_proves1 : list prop1 -> prop1 -> Prop :=
  | SC_init1  Γ P : In P Γ -> SC_proves1 Γ P.

Print False.

Inductive prop : Type :=
| atom_prop : atom -> prop
| bot_prop : prop
| top_prop : prop
| and_prop : prop -> prop  -> prop
| or_prop : prop  -> prop  -> prop
| impl_prop : prop  -> prop  -> prop.

Notation "⊥" := bot_prop.
Notation "⊤" := top_prop.
Infix "∧" := and_prop (left associativity, at level 52).
Infix "∨" := or_prop (left associativity, at level 53).
Infix "⊃" := impl_prop (right associativity, at level 54).

Definition not_prop (P : prop) := P ⊃ ⊥.

Notation "¬ P" := (not_prop P) (at level 51).

Infix "∈" := In (right associativity, at level 55).
Notation "x → y" := (x -> y) (at level 99, y at level 200, right associativity).

Open Scope list_scope.

Reserved Notation "Γ ⇒ P" (no associativity, at level 61).

Inductive SC_proves : list prop -> prop -> Prop :=
| SC_init P Γ : P ∈ Γ → Γ  ⇒ P
| SC_bot_elim P Γ : ⊥ ∈ Γ → Γ ⇒ P
| SC_top_intro Γ : Γ ⇒ ⊤
| SC_and_intro Γ P Q : Γ ⇒ P → Γ ⇒ Q → Γ ⇒ P ∧ Q
| SC_and_elim Γ P Q R : P ∧ Q ∈ Γ → P :: Q :: Γ ⇒ R → Γ ⇒ R
| SC_or_introl Γ P Q :  Γ ⇒ P → Γ ⇒ P ∨ Q
| SC_or_intror Γ P Q : Γ ⇒ Q → Γ ⇒ P ∨ Q
| SC_or_elim Γ P Q R : P ∨ Q ∈ Γ → P :: Γ ⇒ R → Q :: Γ ⇒ R → Γ ⇒ R
| SC_impl_intro Γ P Q : P :: Γ ⇒ Q → Γ ⇒ P ⊃ Q
| SC_impl_elim Γ P Q R : P ⊃ Q ∈ Γ → Γ ⇒ P → Q :: Γ ⇒ R → Γ ⇒ R
  where "Γ ⇒ P" := (SC_proves Γ P).

Notation "⇒ P" := (nil ⇒ P) (no associativity, at level 61).

Theorem PP : forall P, ⇒ P⊃P.
Proof.
intros.
apply SC_impl_intro.
apply SC_init.
simpl. apply or_introl. reflexivity. Qed.

Theorem and_comm : forall P Q, ⇒ P∧Q ⊃ Q∧P.
Proof.
 intros.
 apply SC_impl_intro.
 apply SC_and_intro.
 + apply (SC_and_elim _ P Q _).
    - simpl. apply or_introl. reflexivity.
    - apply SC_init. simpl. apply or_intror. apply or_introl. reflexivity.
 + apply (SC_and_elim _ P Q _).
    - simpl. apply or_introl. reflexivity.
    - apply SC_init. simpl. apply or_introl. reflexivity.
Qed.

Theorem or_comm : forall P Q, ⇒ P∨Q ⊃ Q∨P.
Proof.
  intros.
  apply SC_impl_intro.
  apply (SC_or_elim (P ∨ Q :: nil) P Q (Q ∨ P)).
  + simpl. apply or_introl. reflexivity.
  + apply SC_or_intror. apply SC_init. simpl. apply or_introl. reflexivity.
  + apply SC_or_introl. apply SC_init. simpl. apply or_introl. reflexivity.
Qed.

Theorem PQP : forall P Q, ⇒ P ⊃ Q⊃P.
Proof.
  intros.
  apply SC_impl_intro.
  apply SC_impl_intro.
  apply SC_init.
  simpl. apply or_intror. apply or_introl. reflexivity.
Qed.

Theorem syllogism : forall P Q R, P⊃Q :: Q⊃R :: nil ⇒ P⊃R.
Proof.
  intros.
  apply SC_impl_intro.
  apply (SC_impl_elim _ P Q R).
  +  simpl. apply or_intror. apply or_introl. reflexivity.
  +  apply SC_init. simpl. apply or_introl. reflexivity.
  +  apply (SC_impl_elim _ Q R R).
      -  simpl. apply or_intror. apply or_intror. apply or_intror. apply or_introl. reflexivity.
      -  apply SC_init. simpl. apply or_introl. reflexivity.
      -  apply SC_init. simpl. apply or_introl. reflexivity.
Qed.

Theorem exp : forall P, ⇒ ⊥⊃P.
Proof.
  intros.
  apply SC_impl_intro.
  apply SC_bot_elim.
  simpl. apply or_introl. reflexivity.
Qed.

Definition subcontext (Γ₁ Γ₂ : list (prop)) : Prop :=
forall P, In P Γ₁ -> In P Γ₂.
Infix "⊆" := subcontext (no associativity, at level 70).

Theorem subcontext_provable : forall P Γ', Γ' ⇒ P → forall Γ, Γ' ⊆ Γ → Γ ⇒ P.
Proof.
intros P Γ'.
intros H0.
induction H0.
intros.
apply SC_init. unfold subcontext in H0. apply H0. apply H.
intros. unfold subcontext in H0. apply H0 in H. apply SC_bot_elim. apply H.
intros. apply SC_top_intro. 
intros. apply SC_and_intro. apply IHSC_proves1. apply H.
apply IHSC_proves2. apply H.
intros. 
apply (SC_and_elim _ P Q).
unfold subcontext in H1. apply H1 in H. apply H.
apply IHSC_proves. unfold subcontext. intros.
simpl. simpl in H2. unfold subcontext in H1.
destruct H2.
left. apply H2. destruct H2. right. left. apply H2. right. right. apply H1. apply H2.
intros. apply SC_or_introl. apply IHSC_proves. apply H.
intros. apply SC_or_intror. apply IHSC_proves. apply H.
intros. apply (SC_or_elim _ P Q). unfold subcontext in H0.
apply H0 in H. apply H.
apply IHSC_proves1. unfold subcontext. unfold subcontext in H0.
intros. simpl in H1. simpl. destruct H1. left. apply H1. right. apply H0. apply H1.
apply IHSC_proves2. unfold subcontext. intros. simpl in H1.
destruct H1. simpl. left. apply H1. simpl. right. unfold subcontext in H0. apply H0.
apply H1.
intros. apply SC_impl_intro. apply IHSC_proves. unfold subcontext.
unfold subcontext in H. intros. simpl in H1. destruct H1.
simpl. left. apply H1. simpl. right. apply H. apply H1.
intros. apply (SC_impl_elim _ P Q). unfold subcontext in H0.
apply H0. apply H.
apply IHSC_proves1. apply H0.
apply IHSC_proves2. unfold subcontext. unfold subcontext in H0.
intros. simpl in H1. simpl. destruct H1. left. apply H1.
right. apply H0. apply H1. Qed.

Reserved Notation "Γ ⊢ P" (no associativity, at level 61).

Lemma SC_admits_cut_ext_0 :  forall Γ P, 
  Γ ⇒ P -> P = ⊥ -> forall Q, Γ ⇒ Q.
Proof.
intros Γ P.
intros H.
induction H.
intros.
apply SC_bot_elim. rewrite <- H0. assumption.
intros. apply SC_bot_elim. apply H.
intros. inversion H.
intros. inversion H1.
intros. apply (SC_and_elim _ P Q _).
apply H.
apply IHSC_proves. apply H1.
intros. inversion H0.
intros. inversion H0.
intros.
apply (SC_or_elim _ P Q ). apply H.
apply (IHSC_proves1 H2).
apply IHSC_proves2. apply H2.
intros. inversion H0.
intros. apply (SC_impl_elim _ P Q).
apply H. apply H0. apply IHSC_proves2. apply H2. Qed.


Lemma SC_admits_cut_ext_1 :  forall Γ, 
  Γ ⇒ ⊥ -> forall P, Γ ⇒ P.
Proof.
intros.
apply (SC_admits_cut_ext_0 _ ⊥).
apply H. reflexivity. Qed.


Lemma SC_admits_cut_ext_2 : forall a Γ P,
  Γ ⇒ P -> P = atom_prop a -> forall Q, P::Γ⇒Q -> Γ⇒ Q.
Proof.
intros a Γ P H.
induction H.
intros. apply (subcontext_provable _ (P::Γ)). apply H1.
unfold subcontext. intros. destruct H2.
rewrite <- H2. apply H. apply H2.
intros. apply SC_bot_elim. apply H.
intros. inversion H.
intros. inversion H1.
intros. apply (SC_and_elim _ P Q). apply H.
apply IHSC_proves. apply H1. apply (subcontext_provable _ (R::Γ)). apply H2.
unfold subcontext. intros. simpl.
destruct H3. left. apply H3. right. right. right. apply H3.
intros. inversion H0.
intros. inversion H0.
intros. apply (SC_or_elim _ P Q).
apply H. apply IHSC_proves1. apply H2. apply (subcontext_provable _ (R::Γ)).
apply H3. unfold subcontext.
intros.
simpl. destruct H4. left. apply H4. right. right. apply H4.
apply IHSC_proves2. apply H2. apply (subcontext_provable _ (R::Γ)).
apply H3. unfold subcontext. intros.
simpl. destruct H4. left. apply H4. right. right. apply H4.
intros. inversion H0.
intros. 
apply (SC_impl_elim _ P Q). apply H. apply H0.
apply IHSC_proves2. apply H2. apply (subcontext_provable _ (R::Γ) H3).
unfold subcontext. intros.
simpl. destruct H4. left. apply H4. right. right. apply H4. Qed.

Ltac nrs := (assumption || now repeat subst).
Ltac inveq := match goal with [z: _ = _ |- _] => inversion z end.
Ltac scp z := apply (subcontext_provable _ z).

Ltac uscint := unfold subcontext; intros.
Ltac destincons := subst;match goal with [ z :?x ∈ (_::_)|- ?x ∈ _] => destruct z end; try inveq.
Ltac lr := (left;nrs) || right.
Ltac test := 
    match goal with [z: ?gg∈ ?g |- _ ] =>
        match goal with [zz : g ⊆ _ |- gg ∈ _ ] => unfold subcontext in zz; apply zz in z
        end
    end.

Ltac prove_in := now repeat ( test || destincons || lr || nrs).

Ltac autoscp1 := now
  match goal with [zz: _ |- _  ⇒ ?g] =>
    match goal with 
      | [z :  ?gg ⇒ g |- _] => scp gg
    end
  end ; [assumption | uscint;prove_in].
Ltac autoscp2 := now
  match goal with [zz: _ |- _  ⇒ ?g] =>
    match goal with 
      | [_:_⇒_,z :  ?gg ⇒ g |- _] => scp gg
    end
  end ; [assumption | uscint;prove_in].
Ltac autoscp3 := now
  match goal with [zz: _ |- _  ⇒ ?g] =>
    match goal with 
      | [_:_⇒_,_:_⇒_,z :  ?gg ⇒ g |- _] => scp gg
    end
  end ; [assumption | uscint;prove_in].

Ltac prove_SC := ( assumption ||
now match goal with 
  | [ _ : ?g ⇒ ?gg |- _ ⇒ ?gg ] => (autoscp1 || autoscp2 || autoscp3)
end ||
now match goal with 
  | [ z: ?p ∧ ?q ∈ ?g, zz: ?p::?q::?g ⇒ ?gg|- ?g ⇒ ?gg ] 
       => apply (SC_and_elim _ p q); [ apply z | apply zz ]
  | [ z: ?p ∨ ?q ∈ ?g |- ?g ⇒ _ ] => apply (SC_or_elim _ p q); [ assumption | assumption | assumption ]
end
).

Ltac nowmyauto  := now first [assumption | reflexivity | now inveq | match goal with 
  | [ |- _∈_ ] => prove_in
  | [ |- _⊆_ ] => uscint;prove_in
  | [ |- _ ⇒ _ ] => prove_SC
end ].

Tactic Notation "✓" := nowmyauto.

Ltac tdi := test; destincons; try inveq.

Lemma SC_admits_cut_ext_4 : forall Γ' P,
  Γ' ⇒ P -> forall Γ, Γ' ⊆ ⊤::Γ -> Γ ⇒ P.
Proof.
intros Γ' P H.
induction H.
+
intros. unfold subcontext in H0. apply H0 in H. destruct H. subst.
apply SC_top_intro.
now apply SC_init.
+
intros. unfold subcontext in H0. apply H0 in H. destruct H. inversion H.
now apply SC_bot_elim.
+
intros.
apply SC_top_intro.
+
intros.
apply SC_and_intro. now apply IHSC_proves1.
now apply IHSC_proves2.
+
intros. apply (SC_and_elim _ P Q). ✓. 
apply IHSC_proves. ✓.
+
intros. apply SC_or_introl. now apply IHSC_proves.
+
intros. apply SC_or_intror. now apply IHSC_proves.
+
intros. apply (SC_or_elim _ P Q). ✓.
apply IHSC_proves1. ✓.
apply IHSC_proves2. ✓.
+
intros.
apply SC_impl_intro. apply IHSC_proves.
✓.
+
intros.
apply (SC_impl_elim _ P Q). ✓.
now apply IHSC_proves1.
apply IHSC_proves2. ✓.
Qed.

Lemma SC_admits_cut_ext_5 : forall Γ P,
  ⊤::Γ ⇒ P -> Γ ⇒ P.
Proof.
intros.
apply (SC_admits_cut_ext_4 (⊤::Γ)).
apply H. ✓. Qed.

Lemma SC_admits_cut_ext : forall P,
  forall Γ' Q, Γ' ⇒ Q -> forall Γ, Γ ⇒ P -> Γ' ⊆ P :: Γ -> Γ ⇒ Q.
Proof.
intros P. induction P.
+ intros Γ' Q H. induction H.
- intros.
unfold subcontext in H1. apply H1 in H. destruct H.
rewrite <- H. apply H0. apply SC_init. ✓.
- intros. unfold subcontext in H1. apply H1 in H.
destruct H. inversion H. apply SC_bot_elim. ✓.
-  intros. apply SC_top_intro.
- intros. apply SC_and_intro. apply IHSC_proves1.
assumption. ✓. 
apply IHSC_proves2. apply H1. ✓.
- intros Γ0 H1. intros.
apply (SC_and_elim _ P Q). ✓. 
apply IHSC_proves. ✓. ✓.
- intros. apply (SC_or_introl). apply IHSC_proves.
assumption. ✓.
- intros. apply (SC_or_intror). apply IHSC_proves. apply H0. ✓.
- intros. apply (SC_or_elim _ P Q). ✓.
apply IHSC_proves1. ✓. ✓.
apply IHSC_proves2. ✓. ✓.
-
intros. apply SC_impl_intro. apply IHSC_proves. ✓. ✓.
-
intros.
apply (SC_impl_elim _ P Q). ✓.
apply IHSC_proves1. ✓. ✓.
apply IHSC_proves2. ✓. ✓.
+
intros.
apply SC_admits_cut_ext_1. apply H0.
+
intros. apply SC_admits_cut_ext_5. ✓.
+
intros Γ' Q H.
induction H.
-
intros.
unfold subcontext in H1.
apply H1 in H. 
inversion H. rewrite <-H2. apply H0.
apply SC_init. ✓.
-
intros. unfold subcontext in H1. apply H1 in H. inversion H.
inversion H2. apply SC_bot_elim. ✓. 
-
intros. apply SC_top_intro.
-
intros. apply SC_and_intro. apply IHSC_proves1.
apply H1. ✓. apply IHSC_proves2. apply H1. ✓.
-
intros Γ0 H1.
remember (P1∧P2) as P3.
induction H1.
* intros. apply (subcontext_provable _ Γ). prove_SC. uscint. test. destincons. assumption. assumption.
* intros. apply SC_bot_elim. apply H1.
* intros. ✓.
* intros. 
apply H1 in H. inversion H.
{
inversion HeqP3. subst. inversion H2. subst.
apply (IHP2 (Q::Γ0)). 
apply (IHP1 (P::Q::Γ0)).
apply IHSC_proves. apply SC_and_intro.
apply SC_init. ✓.
apply SC_init. ✓. ✓.
✓. ✓. ✓. ✓.
}{ 
apply (SC_and_elim _ P Q). ✓. 
apply IHSC_proves.
apply SC_and_intro. inveq. subst. ✓. ✓. ✓.
}
*
intros.
apply (SC_and_elim _ P0 Q0). ✓.
apply IHSC_proves0. assumption. intros.
apply IHSC_proves; assumption. ✓.
*
inversion HeqP3.
*
inversion HeqP3.
*
intros.
apply H2 in H.
destruct H. 
{
subst.
inversion HeqP3. subst.
apply (SC_or_elim _ P0 Q0). ✓.
apply IHSC_proves1.
reflexivity.
intros.
apply IHSC_proves. apply H. ✓. ✓.
apply IHSC_proves2. reflexivity.
intros.
apply IHSC_proves. apply H. ✓. ✓.
}{
apply (SC_and_elim _ P Q). ✓.
apply IHSC_proves. apply (SC_or_elim _ P0 Q0). ✓.
apply (subcontext_provable _ (P0::Γ0)). ✓. ✓. ✓. ✓.
}
*
intros.
inversion HeqP3.
* intros.
apply (SC_impl_elim _ P0 Q0). ✓. assumption.
apply IHSC_proves2. assumption. intros.
apply (IHSC_proves _ H3). ✓. ✓.
-
intros. apply (SC_or_introl).
apply IHSC_proves; assumption.
-
intros. apply (SC_or_intror).
apply IHSC_proves; assumption.
-
intros Γ0 H2.
intros.
apply H3 in H.
destruct H. inversion H.
apply (SC_or_elim _ P Q). ✓.
apply IHSC_proves1. ✓. ✓.
apply IHSC_proves2. ✓. ✓.
- intros.
apply SC_impl_intro.
apply IHSC_proves. ✓. ✓.
- intros.
apply H3 in H. destruct H. inversion H.
apply (SC_impl_elim _ P Q). ✓. 
apply IHSC_proves1. ✓. ✓.
apply IHSC_proves2. ✓. ✓.
+
intros Γ' Q H.
remember (P1∨P2) as R.
induction H.
-
intros. subst.
unfold subcontext in H1. apply H1 in H. destruct H.
rewrite <- H. assumption.
apply SC_init. ✓.
-
intros. subst. unfold subcontext in H1. apply H1 in H.
destruct H. inversion H. apply SC_bot_elim. ✓.
- intros. apply SC_top_intro.
- intros. subst. apply SC_and_intro. apply IHSC_proves1. ✓. ✓.
apply IHSC_proves2. ✓. ✓.
- intros. subst. apply H2 in H. destruct H. inversion H.
apply (SC_and_elim _ P Q). ✓. apply IHSC_proves. ✓. ✓.
-
intros. subst. apply SC_or_introl. apply IHSC_proves. ✓. ✓.
- intros. apply SC_or_intror. apply IHSC_proves. ✓. ✓.
- intros Γ0 H2.
induction H2.
* intros. apply (subcontext_provable _ Γ). prove_SC. ✓.
* intros. apply SC_bot_elim. ✓.
* intros. inversion HeqR.
* inversion HeqR.  
* intros. apply (SC_and_elim _ P0 Q0). ✓. 
 apply IHSC_proves. ✓. intros. apply IHSC_proves1. ✓. ✓. intros. apply IHSC_proves2. ✓. ✓. ✓.
* intros. inversion HeqR. subst. apply H3 in H.
destruct H.
{ inversion H. subst. apply (IHP1 (P::Γ0)). apply IHSC_proves1. apply (subcontext_provable _ Γ0).
apply SC_or_introl. apply H2. ✓. ✓. ✓. ✓. }
{ apply (SC_or_elim _ P Q). ✓. apply IHSC_proves1. 
apply (subcontext_provable _ Γ0). apply SC_or_introl. apply H2. ✓. ✓.
apply IHSC_proves2. apply (subcontext_provable _ Γ0). apply SC_or_introl. apply H2.
✓. ✓. }
* intros. inversion HeqR. apply H3 in H. destruct H.
{ inversion H. subst. subst. apply (IHP2 (Q::Γ0)). apply IHSC_proves2. apply SC_or_intror.
apply SC_init. ✓. ✓. ✓. ✓. }
{ apply (SC_or_elim _ P Q). ✓. apply IHSC_proves1. apply SC_or_intror. ✓. ✓.
apply IHSC_proves2.
apply (subcontext_provable _ Γ0).
apply SC_or_intror. apply H2. ✓. ✓.
} 
*
intros. apply H3 in H. destruct H. 
{
subst. inversion HeqR. subst. apply (SC_or_elim _ P0 Q0). ✓.
apply IHSC_proves3. reflexivity. intros. apply IHSC_proves1.  apply H. ✓.
intros. apply IHSC_proves2. apply H. ✓. ✓.
apply IHSC_proves4. reflexivity. intros. apply IHSC_proves1. apply H. ✓.
intros. apply IHSC_proves2. apply H. ✓. ✓. }
{
subst. apply (SC_or_elim _ P0 Q0). ✓. apply IHSC_proves3.
reflexivity. intros.  apply IHSC_proves1. ✓. ✓. intros. apply IHSC_proves2.
apply H4. ✓. ✓. 
apply (IHSC_proves4). reflexivity. intros. apply IHSC_proves1. ✓. ✓. intros. 
apply IHSC_proves2. ✓. ✓. ✓.
} 
*
intros. inversion HeqR.
* intros. apply H3 in H. destruct H.
{ subst. inversion HeqR. subst. 
apply (SC_impl_elim _ P0 Q0). ✓. ✓. apply IHSC_proves4. reflexivity. intros.
apply IHSC_proves1. apply H. ✓. intros. apply IHSC_proves2. ✓. ✓. ✓.
}
{ subst. apply (SC_or_elim _ P Q). ✓. apply IHSC_proves1.
apply (SC_impl_elim _ P0 Q0). ✓. ✓. ✓. ✓.
apply IHSC_proves2. apply (SC_impl_elim _ P0 Q0). ✓. ✓. ✓. ✓.
} 
-
intros.
apply SC_impl_intro.
subst. apply IHSC_proves. ✓. ✓.
-
intros.
subst. apply H3 in H. destruct H. inversion H.
apply (SC_impl_elim _ P Q). ✓. apply IHSC_proves1. ✓. ✓.
apply IHSC_proves2. ✓. ✓.
+
intros Γ' Q H. induction H.
-
intros. unfold subcontext in H1. apply H1 in H. destruct H. rewrite<- H. apply H0. apply SC_init.
apply H.
- intros. unfold subcontext in H1. apply H1 in H. destruct H. inversion H. apply SC_bot_elim. apply H.
- intros. apply SC_top_intro.
-intros. apply SC_and_intro. apply IHSC_proves1. apply H1. apply H2. apply IHSC_proves2.
apply H1. apply H2.
- intros. apply (SC_and_elim _ P Q). unfold subcontext in H2. apply H2 in H. destruct H.
inversion H. apply H. apply IHSC_proves. apply (subcontext_provable _ Γ0). apply H1.
unfold subcontext. intros. right. now right.
unfold subcontext. intros. destruct H3. right. now left. destruct H3. right. right. now left.
unfold subcontext in H2. apply H2 in H3. destruct H3. now left. right. right. now right.
-
intros. apply SC_or_introl. apply IHSC_proves. apply H0. apply H1.
-  intros. apply SC_or_intror. apply IHSC_proves. apply H0. apply H1.
- intros.  apply (SC_or_elim _ P Q). unfold subcontext in H3. apply H3 in H. destruct H. inversion H.
apply H. apply IHSC_proves1. apply (subcontext_provable _ Γ0). apply H2. unfold subcontext.
intros. now right. unfold subcontext. intros. destruct H4. right. now left.
unfold subcontext in H3. apply H3 in H4. destruct H4. now left. right. now right.
apply IHSC_proves2. apply (subcontext_provable _ Γ0).
apply H2. unfold subcontext. intros. now right.
unfold subcontext. intros. destruct H4. right. now left. unfold subcontext in H3. apply H3 in H4.
destruct H4. now left. right. now right.
-
intros. apply SC_impl_intro. apply IHSC_proves. apply (subcontext_provable _ Γ0).
apply H0. unfold subcontext. intros. now right.
 unfold subcontext. intros. destruct H2. right. now left. unfold subcontext in H1. apply H1 in H2.
destruct H2. left. assumption. right. now right.
-
intros Γ0 H2. remember (P1⊃P2) as S.
induction H2.
* intros. apply (SC_impl_elim _ P Q). unfold subcontext in H3. apply H3 in H.
destruct H. now rewrite <-H. now apply H. apply IHSC_proves1. apply SC_init. apply H2.
apply H3. apply IHSC_proves2. apply SC_init. now right. 
unfold subcontext. intros. unfold subcontext in H3. destruct H4. right. now left.
apply H3 in H4. destruct H4. now left. right. now right.
*
intros. apply SC_bot_elim. apply H2.
*
intros. apply (SC_impl_elim _ P Q). unfold subcontext in H2. apply H2 in H. destruct H.
inversion H. apply H. apply IHSC_proves1. apply SC_top_intro. apply H2.
apply IHSC_proves2. apply SC_top_intro. unfold subcontext. intros. destruct H3. right. now left.
unfold subcontext in H2. apply H2 in H3. destruct H3. now left. right. now right.
*
intros. apply (SC_impl_elim _ P Q). unfold subcontext in H2. apply H2 in H.
destruct H. inversion H.
apply H.
apply IHSC_proves1. apply SC_and_intro; assumption.
unfold subcontext. intros. unfold subcontext in H2. apply H2 in H3. destruct H3. now left.
now right.
apply IHSC_proves2. apply (subcontext_provable _ Γ0). apply SC_and_intro.
apply H2_. apply H2_0. unfold subcontext. intros. now right.
unfold subcontext. intros. destruct H3. right. now left. unfold subcontext in H2. apply H2 in H3.
destruct H3. now left. right. now right.
*
intros. subst.
apply (SC_and_elim _ P0 Q0). apply H2. apply IHSC_proves.
intros. reflexivity. apply IHSC_proves1. intros. apply IHSC_proves2.
apply H5. apply H6.
intros.
unfold subcontext. intros. unfold subcontext in H4. apply H4 in H5.
destruct H5. now left. right. right. now right.
*
intros.
unfold subcontext in H3. apply H3 in H. destruct H. inversion H.
apply (SC_impl_elim _ P Q). apply H. apply IHSC_proves1.
apply SC_or_introl. assumption.
unfold subcontext. assumption. apply IHSC_proves2. apply (subcontext_provable _ Γ0).
apply SC_or_introl. apply H2. unfold subcontext. intros. right. assumption.
unfold subcontext. intros. destruct H4. right. now left. apply H3 in H4. destruct H4.
now left. right. now right.
*
intros.
unfold subcontext in H3. apply H3 in H. destruct H. inversion H.
apply (SC_impl_elim _ P Q). apply H. apply IHSC_proves1.
apply SC_or_intror. assumption.
unfold subcontext. assumption. apply IHSC_proves2. apply (subcontext_provable _ Γ0).
apply SC_or_intror. apply H2. unfold subcontext. intros. right. assumption.
unfold subcontext. intros. destruct H4. right. now left. apply H3 in H4. destruct H4.
now left. right. now right.
*
intros. subst. apply (SC_or_elim _ P0 Q0). assumption. apply IHSC_proves3. intros.
reflexivity. 
unfold subcontext. intros. unfold subcontext in H3. apply IHSC_proves1. apply H4. 
unfold subcontext.
apply H5. intros.
apply IHSC_proves2. apply H4. apply H5.
unfold subcontext. intros. unfold subcontext in H3. apply H3 in H4. destruct H4. now left. right.
now right. apply IHSC_proves4. reflexivity.
intros. apply IHSC_proves1. apply H4. apply H5. intros. apply IHSC_proves2. apply H4.
apply H5. unfold subcontext. unfold subcontext in H3. intros. apply H3 in H4. destruct H4. now left.
right. now right.
*
intros.
unfold subcontext in H3. 
apply H3 in H. destruct H. 
{ inversion H. subst.
inversion HeqS. subst.
apply (IHP2 (P2::Γ0)). apply IHSC_proves2. apply SC_impl_intro. 
apply (subcontext_provable _ (P1::Γ0)). apply H2. unfold subcontext. intros. destruct H4.
now left. right. now right.
unfold subcontext. intros. destruct H4. right. now left. apply H3 in H4. destruct H4. now left.
right. now right.
apply (IHP1 (P1::Γ0)). apply H2. apply IHSC_proves1. apply SC_impl_intro. apply H2.
unfold subcontext. apply H3. unfold subcontext. intros. assumption. unfold subcontext. intros.
assumption.
}
{
inversion HeqS. subst.
apply (SC_impl_elim _ P Q). apply H. apply IHSC_proves1. apply SC_impl_intro.
apply H2. unfold subcontext. apply H3.
apply IHSC_proves2. apply (subcontext_provable _ Γ0). apply SC_impl_intro. apply H2.
unfold subcontext. intros. now right.
unfold subcontext. intros. destruct H4. right. now left.
apply H3 in H4. destruct H4. now left. right. now right.
}
*
intros.
subst.
unfold subcontext in H3. apply H3 in H. destruct H.
{
inversion H. subst.
apply (SC_impl_elim _ P0 Q0). apply H2. apply H2_. apply IHSC_proves4.
reflexivity. intros. apply IHSC_proves1. apply H4. apply H5.
intros. apply IHSC_proves2. apply H4. apply H5. unfold subcontext.
intros. apply H3 in H4. destruct H4. now left. right. now right.
}
{
apply (SC_impl_elim _ P Q). apply H. apply IHSC_proves1. 
apply (SC_impl_elim _ P0 Q0). assumption. assumption. assumption. unfold subcontext.
assumption. apply IHSC_proves2. 
apply (SC_impl_elim _ P0 Q0). right. apply H2.
apply (subcontext_provable _ Γ0). apply H2_. unfold subcontext. intros. now right.
apply (subcontext_provable _ (Q0::Γ0)). apply H2_0. unfold subcontext. intros. destruct H4.
now left. right. now right.  unfold subcontext. intros. destruct H4. right. now left. apply H3 in H4.
destruct H4. now left. right. now right. } Qed.

Theorem SC_admits_cut : forall Γ P Q,
  Γ ⇒ P -> P :: Γ ⇒ Q -> Γ ⇒ Q.
Proof.
intros.
apply (SC_admits_cut_ext P (P::Γ)).
apply H0. apply H. unfold subcontext. intros. apply H1. Qed.