Admissibility of cut for simple intuitionistic sequent calculus
cut.lf
proptm : type.
top : proptm.
imp : {A:proptm}{B:proptm}proptm.
and : {A:proptm}{B:proptm}proptm.
hyp : {A:proptm} type.
conc : {C:proptm} type.
init : {A:proptm}{D:hyp A}conc A.
topR : conc top.
andL : {A:proptm}{B:proptm}{C:proptm}{D1:{x:hyp A}{y:hyp B}conc C}
{D2:hyp (and A B)} conc C.
andR : {A:proptm}{B:proptm}{D1:conc A}{D2:conc B}
conc (and A B).
impL : {A:proptm}{B:proptm}{C:proptm}{D1:conc A}{D2:{x:hyp B}conc C}
{D3:hyp (imp A B)}conc C.
impR : {A:proptm}{B:proptm}{D:{x:hyp A}conc B}
conc (imp A B).cut.ath
Specification "cut.lf".
Schema c :=
{A}(x:hyp A).
Theorem imp_inv : ctx G:c, forall A B D,
{G |- D : conc (imp A B)} =>
exists D':o -> o, {G |- [x] D' x : {x:hyp A}conc B}.
induction on 1. intros. case H1(keep).
%case 1: impR
exists D1. search.
%case 2: impL
apply IH to H6 with (G = G,n:hyp B1), A = A, B = B, D = D2 n.
exists ([x] impL A1 B1 B D1 ([y] D' y x) D3).
case H4(keep). weaken H2 with (hyp A). weaken H3 with (hyp A).
weaken H10 with (hyp A). weaken H5 with (hyp A).
ctxpermute H8 to G, n1:hyp A, n:hyp B1. weaken H7 with (hyp A).
search.
%case 3: andL
apply IH to H5 with (G = G, n:hyp A1, n1:hyp B1).
ctxpermute H7 to G, n2:hyp A, n:hyp A1, n1:hyp B1.
exists ([x] andL A1 B1 B ([y][z] D' z y x) D2).
case H4(keep). weaken H2 with (hyp A). weaken H3 with (hyp A). weaken H6 with (hyp A).
weaken H10 with (hyp A).
search.
%case 4: init
case H3.
exists ([x] impL (A n) (B n) (B n) (init (A n) x) ([y] init (B n) y) n).
case H2(keep). weaken H4 with (hyp (A n)). weaken H5 with (hyp (A n)).
weaken H7 with (hyp (B n)).
search.
Theorem and_inv : ctx G:c, forall A B D,
{G |- D : conc (and A B)} =>
exists D1 D2, {G |- D1 : conc A} /\ {G |- D2 : conc B}.
induction on 1. intros. case H1(keep).
%case 1: impL
apply IH to H6 with (G = G, n:hyp B1), A = A, B = B, D = D2 n.
case H8.
exists impL A1 B1 A D1 ([y] D4 y) D3.
exists impL A1 B1 B D1 ([y] D5 y) D3.
split.
%case 1.1: left (A)
case H4(keep). search.
%case 1.2: right (B)
case H4(keep). search.
%case 2: andR
exists D1. exists D2. split. search. search.
%case 3: andL
apply IH to H5 with (G = G, n:hyp A1, n1:hyp B1), A = A, B = B, D = (D1 n n1).
case H7.
exists (andL A1 B1 A ([x][y] D3 y x) D2).
exists (andL A1 B1 B ([x][y] D4 y x) D2).
split.
%case 3.1: left(A)
case H4(keep). search.
%case 3.2: right(B)
case H4(keep). search.
%case 4: init
case H3. case H2.
exists (andL (A n) (B n) (A n) ([x][y] init (A n) x) n).
exists (andL (A n) (B n) (B n) ([x][y] init (B n) y) n).
split.
%case 4.1: left((A n))
weaken H4 with (hyp (A n)). weaken H5 with (hyp (A n)). weaken H6 with (hyp (B n)). search.
%case 4.2: right((B n))
weaken H5 with (hyp (A n)). weaken H6 with (hyp (B n)). search.
Theorem cut : ctx G:c, forall A B D1 D2: o -> o,
{A : proptm} => {G |- D1 : conc A} => {G |- [x] D2 x : {x:hyp A} conc B} =>
exists D3, {G |- D3 : conc B}.
induction on 1. induction on 3. intros.
case H3(keep).
%case 1: impR
ctxpermute H6 to G, n1:hyp B1, n:hyp A.
strengthen H4. strengthen H5. weaken H2 with (hyp B1).
apply IH1 to H1 H10 H7 with (G = G, n2:hyp B1), A = A, B = B2, D1 = D1, D2 = ([x]D x n2).
exists (impR B1 B2 ([x:o] D3 x n1 n)). search.
%case 2: impL
case H9(keep).
%case 2.1: essential case
case H1(keep). apply imp_inv to H2.
apply IH1 to H1 H2 H7 with (G = G), A = (imp A2 A3), B = A2, D1 = D1, D2 = D3.
apply IH to H10 H13 H12 with (G = G), A = A2, B = A3, D1 = D2 n2 n1 n, D2 = ([x] D' n1 n x).
ctxpermute H8 to G, n1:hyp A3, n: hyp (imp A2 A3).
strengthen H5. weaken H2 with (hyp A3).
apply IH1 to H1 H17 H15 with (G = G, n1:hyp A3), A = (imp A2 A3), B = B, D1 = D1, D2 = [x] D4 x n1.
apply IH to H11 H14 H18 with (G = G), A = A3, B = B, D1 = D5 n2 n1 n, D2 = [x] D6 n3 n2 x n.
exists D7 n3 n2 n1 n. search.
%case 2.2: commutative case
apply IH1 to H1 H2 H7 with (G = G), A = (A n2), B = A3 n2, D1 = D1 n2, D2 = [x] D3 n2 x.
ctxpermute H8 to G, n1:hyp (A4 n2), n:hyp (A n2).
strengthen H5. weaken H2 with (hyp (A4 n2)).
apply IH1 to H1 H13 H11 with (G = G, n1:hyp (A4 n2)), A = (A n2), B = (B n2), D1 = (D1 n2), D2 = [x] D4 n2 x n1.
strengthen H4. strengthen H5. strengthen H6.
exists (impL (A3 n2) (A4 n2) (B n2) (D2 n2 n1 n) ([x]D5 n3 n2 x n) n2). search.
%case 3: andR
apply IH1 to H1 H2 H6 with A = A, B = B1, D1 = D1, D2 = D3.
apply IH1 to H1 H2 H7 with A = A, B = B2, D1 = D1, D2 = D4.
strengthen H4. strengthen H5.
exists (andR B1 B2 (D2 n) (D5 n)). search.
%case 4: andL
case H8(keep).
%case 4.1: essential case
case H1(keep). apply and_inv to H2. case H11.
ctxpermute H7 to G, n1:hyp A2, n2:hyp A3, n:hyp (and A2 A3).
assert {G, n1:hyp A2, n2:hyp A3 |- D1 : conc (and A2 A3)}.
strengthen H4. strengthen H5.
weaken H2 with (hyp A2). weaken H16 with (hyp A2). weaken H17 with (hyp A3).
search.
apply IH1 to H1 H15 H14 with (G = G, n1:hyp A2, n2:hyp A3), A = (and A2 A3), B = B, D1 = D1, D2 = [x] D3 x n1 n2.
assert {G |- [x] D4 n2 n1 n : {x: hyp A2} conc A3}.
strengthen H4.
weaken H13 with (hyp A2). search.
%%%%Check this out more for possible naming issue
apply IH to H10 H17 H16 with (G = G, n1:hyp A2), A = A3, B = B, D2 = [x] D5 x n1 n.
%%%%
apply IH to H9 H12 H18.
exists D7 n3 n2 n1 n. search.
%case 4.2: commutative case
ctxpermute H7 to G, n1:hyp (A3 n3), n2:hyp (A4 n3), n:hyp (A n3).
assert {G, n1:hyp (A3 n3), n2:hyp (A4 n3) |- D1 n3 : conc (A n3)}.
strengthen H4. strengthen H5.
weaken H2 with (hyp (A3 n3)). weaken H11 with (hyp (A3 n3)). weaken H12 with (hyp (A4 n3)).
search.
apply IH1 to H1 H10 H9 with (G = G, n1:hyp (A3 n3), n2:hyp (A4 n3)), A = (A n3), B = (B n3), D1 = (D1 n3), D2 = [x] D3 n3 x n1 n2.
exists (andL (A3 n3) (A4 n3) (B n3) ([x][y] D2 n3 y x n) n3).
strengthen H4. strengthen H5. strengthen H6. search.
%case 5: topR
exists topR. search.
%case 6: init
case H5.
%case 6.1: n
exists D1. search.
%case 6.2: n1 from earlier in context
strengthen H3. exists (init (B n1) n1). search.