-
Notifications
You must be signed in to change notification settings - Fork 0
/
ST3.v
118 lines (105 loc) · 4.87 KB
/
ST3.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
Require Import List.
Require Import lang.
Import List.ListNotations.
Definition max := PeanoNat.Nat.max.
Reserved Notation "G '⇒3' D '⨡' n " (no associativity, at level 61). (* 21d2, 2a21 *)
Inductive ST3 : nat -> sequent -> Prop :=
| TId: forall (p : atom) G, ^x_p :: G ⇒3 ^x_p ⨡ 0
| TRT: forall G, G ⇒3 ⊤ ⨡ 0
| TLF: forall G D, ⊥ :: G ⇒3 D ⨡ 0
| TLw: forall G D P n, G ⇒3 D ⨡ n -> G ++ P ⇒3 D ⨡ S n
| TRw: forall G a n, G ⇒3 None ⨡ n -> G ⇒3 a ⨡ S n
| TLa: forall G D (a b : form) n, a::b::G ⇒3 D ⨡ n -> (a ∧ b)::G ⇒3 D ⨡ S n
| TRa: forall G (a b : form) n m, G ⇒3 a ⨡ n -> G ⇒3 b ⨡ m -> G ⇒3 (a ∧ b) ⨡ S (max n m)
| TLo: forall G D (a b : form) n m, a::G ⇒3 D ⨡ n -> b::G ⇒3 D ⨡ m -> (a ∨ b)::G ⇒3 D ⨡ S (max n m)
| TRo1: forall G (a b : form) n, G ⇒3 a ⨡ n -> G ⇒3 (a ∨ b) ⨡ S n
| TRo2: forall G (a b : form) n, G ⇒3 b ⨡ n -> G ⇒3 (a ∨ b) ⨡ S n
| TLi: forall G D (a b : form) n m, ∇(a ⊃ b)::G ⇒3 a ⨡ n -> ∇(a ⊃ b)::b::G ⇒3 D ⨡ m -> ∇(a ⊃ b)::G ⇒3 D ⨡ S (max n m)
| TRi: forall G (a b : form) n, a::(∇l G) ⇒3 b ⨡ n -> G ⇒3 (a ⊃ b) ⨡ S n
| TN: forall G a n, G ⇒3 Some a ⨡ n -> ∇l G ⇒3 Some (∇ a) ⨡ S n
| TEx: forall G P D a b n, G++a::b::P ⇒3 D ⨡ n -> G++b::a::P ⇒3 D ⨡ S n
where "G ⇒3 D ⨡ n" := (ST3 n (Seq G D)).
Notation "⇒3 a ⨡ n" := ([] ⇒3 a ⨡ n) (no associativity, at level 62).
Reserved Notation "G ⇒3+ D ⨡ n" (no associativity, at level 61). (* 21d2, 2a21 *)
Inductive ST3p : nat -> sequent -> Prop :=
| PTId: forall (p : atom) G, ^x_p :: G ⇒3+ ^x_p ⨡ 0
| PTRT: forall G, G ⇒3+ ⊤ ⨡ 0
| PTLF: forall G D, ⊥ :: G ⇒3+ D ⨡ 0
| PTLw: forall G D P n, G ⇒3+ D ⨡ n -> G ++ P ⇒3+ D ⨡ S n
| PTRw: forall G a n, G ⇒3+ None ⨡ n -> G ⇒3+ a ⨡ S n
| PTLa: forall G D (a b : form) n, a::b::G ⇒3+ D ⨡ n-> (a ∧ b)::G ⇒3+ D ⨡ S n
| PTRa: forall G (a b : form) n m, G ⇒3+ a ⨡ n -> G ⇒3+ b ⨡ m-> G ⇒3+ (a ∧ b) ⨡ S (max n m)
| PTLo: forall G D (a b : form) n m, a::G ⇒3+ D ⨡ n -> b::G ⇒3+ D ⨡ m -> (a ∨ b)::G ⇒3+ D ⨡ S (max n m)
| PTRo1: forall G (a b : form) n, G ⇒3+ a ⨡ n -> G ⇒3+ (a ∨ b) ⨡ S n
| PTRo2: forall G (a b : form) n, G ⇒3+ b ⨡ n -> G ⇒3+ (a ∨ b) ⨡ S n
| PTLi: forall G D (a b : form) n m, ∇(a ⊃ b)::G ⇒3+ a ⨡ n -> ∇(a ⊃ b)::b::G ⇒3+ D ⨡ m -> ∇(a ⊃ b)::G ⇒3+ D ⨡ S (max n m)
| PTRi: forall G (a b : form) n, a::(∇l G) ⇒3+ b ⨡ n -> G ⇒3+ (a ⊃ b) ⨡ S n
| PTN: forall G a n, G ⇒3+ Some a ⨡ n -> ∇l G ⇒3+ Some (∇ a) ⨡ S n
| PTEx: forall G P D a b n, G++a::b::P ⇒3+ D ⨡ n -> G++b::a::P ⇒3+ D ⨡ S n
| Cut: forall (a : form) G P D n m, G ⇒3+ a ⨡ n -> a::P ⇒3+ D ⨡ m -> G++P ⇒3+ D ⨡ S (max n m)
where "G ⇒3+ D ⨡ n" := (ST3p n (Seq G D)).
Notation "⇒3+ a ⨡ n" := ([] ⇒3+ a ⨡ n) (no associativity, at level 62).
Lemma ST3_ST3p : forall n {s : sequent}, ST3 n s -> ST3p n s.
Proof.
intros n s H. induction H.
- apply PTId.
- apply PTRT.
- apply PTLF.
- apply PTLw. apply IHST3.
- apply PTRw. apply IHST3.
- apply PTLa. apply IHST3.
- apply PTRa.
+ apply IHST3_1.
+ apply IHST3_2.
- apply PTLo.
+ apply IHST3_1.
+ apply IHST3_2.
- apply PTRo1. apply IHST3.
- apply PTRo2. apply IHST3.
- apply PTLi.
+ apply IHST3_1.
+ apply IHST3_2.
- apply PTRi. apply IHST3.
- apply PTN. apply IHST3.
- apply PTEx. apply IHST3.
Defined.
Coercion ST3_ST3p : ST3 >-> ST3p.
Tactic Notation "swap_hd" := apply (TEx [] _ _ _ _); simpl.
Theorem ST3_Id: forall (a : form) (G : context), exists n, a::G ⇒3 a ⨡ n.
Proof.
intros a.
induction a; intros G.
- exists 0. apply TId.
- exists 0. apply TLF.
- exists 0. apply TRT.
- assert (this: ∇ a :: G = [∇ a] ++ G).
{ reflexivity. }
rewrite this.
destruct (IHa []) as [n IHan]. exists (2 + n).
apply TLw.
rewrite nabla_singleton.
apply TN.
apply IHan.
- destruct (IHa1 G) as [n IHa1n].
destruct (IHa2 G) as [m IHa2m].
exists (S (max (S n) (S m))).
apply TLo.
+ apply TRo1. apply IHa1n.
+ apply TRo2. apply IHa2m.
- destruct (IHa1 (a2::G)) as [n IHa1n].
destruct (IHa2 (a1::G)) as [m IHa2m].
exists (S (S (max n (S m)))).
apply TLa. apply TRa.
+ apply IHa1n.
+ swap_hd. apply IHa2m.
- destruct (IHa1 (∇ (a1 ⊃ a2) :: ∇l G)) as [n IHa1n].
destruct (IHa2 (∇ (a1 ⊃ a2) :: a1 :: ∇l G)) as [m IHa2m].
exists (S (S (S (max (S n) (S m))))).
apply TRi. simpl "∇l".
remember (max (S n) (S m)) as q.
swap_hd.
rewrite Heqq.
apply TLi.
+ swap_hd. apply IHa1n.
+ swap_hd. apply IHa2m.
Qed.