Skip to content

Commit f8f00b9

Browse files
radumcostacheradumcostache
committed
Added:
- Examples. Modified: - Makefile - improved documentation
1 parent 15edc54 commit f8f00b9

File tree

4 files changed

+403
-186
lines changed

4 files changed

+403
-186
lines changed

‎Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ HASNATDYNLINK := $(COQMF_HASNATDYNLINK)
4545
OCAMLWARN := $(COQMF_WARN)
4646

4747
Makefile.conf: _CoqProject
48-
coq_makefile -f _CoqProject src/Sequents.v src/SequentsVLSM.v -o Makefile
48+
coq_makefile -f _CoqProject src/Examples.v src/Sequents.v src/SequentsVLSM.v -o Makefile
4949

5050
# This file can be created by the user to hook into double colon rules or
5151
# add any other Makefile code he may need

‎src/Examples.v‎

Lines changed: 186 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,186 @@
1+
From stdpp Require Import prelude.
2+
From VLSM.Core Require Import VLSM Composition ProjectionTraces.
3+
From VLSM_SC Require Import Sequents.
4+
From VLSM_SC Require Import SequentsVLSM.
5+
6+
Import Form.
7+
Import Calculus.
8+
9+
#[local] Notation "⊤" := FTop.
10+
#[local] Notation "⊥" := FBot.
11+
#[local] Notation "x ∨ y" := (FDisj x y) (at level 85, right associativity).
12+
#[local] Notation "x ∧ y" := (FConj x y) (at level 80, right associativity).
13+
#[local] Notation "x → y" := (FImpl x y) (at level 99, y at level 200, right associativity).
14+
15+
(** * Examples *)
16+
17+
(** ** The derivation of Peirce's Law in GK' *)
18+
19+
Example derivable_peirce :
20+
forall (A B : Formula), derivable_sequent(seq [] [((A→B)→A)→A]).
21+
Proof.
22+
intros A B.
23+
exists 5.
24+
apply SC_IMP_RIGHT.
25+
apply SC_CT_RIGHT.
26+
cut (SC_derivation 0 (seq [A] [A])).
27+
- intros HAID.
28+
apply (SC_IMP_LEFT (A→B) A [] [] [A] [A] 2 0).
29+
+ apply SC_IMP_RIGHT.
30+
by apply SC_WK_RIGHT.
31+
+ exact HAID.
32+
- apply SC_ID.
33+
Qed.
34+
35+
(** ** The valid VLSM trace of Peirce's Law *)
36+
37+
Definition peirce_trace_pref (A B : Formula) : list (transition_item sequent_vlsm) :=
38+
[@Build_transition_item Sequent sequent_vlsm (existT I_V_ID A) (None) s0_seq (Some (seq [A] [A]));
39+
@Build_transition_item Sequent sequent_vlsm (existT I_V_WK_RIGHT B) (Some (seq [A] [A])) s0_seq (Some (seq [A] [B; A]));
40+
@Build_transition_item Sequent sequent_vlsm (existT I_V_IMP_RIGHT ()) (Some (seq [A] [B; A])) s0_seq (Some (seq [] [A→B; A]));
41+
@Build_transition_item Sequent sequent_vlsm (existT I_V_IMP_LEFT recLeft) (Some (seq [A] [A]))
42+
(state_update sequent_vlsm_components s0_seq I_V_IMP_LEFT (Some (seq [A] [A])) ) (None);
43+
@Build_transition_item Sequent sequent_vlsm (existT I_V_IMP_LEFT emitLeft) (Some (seq [] [A→B; A])) s0_seq (Some (seq [(A→B)→A] [A; A]));
44+
@Build_transition_item Sequent sequent_vlsm (existT I_V_CT_RIGHT ()) (Some (seq [(A→B)→A] [A; A])) s0_seq (Some (seq [(A→B)→A] [A]))
45+
].
46+
47+
Definition peirce_trace_last (A B : Formula): transition_item sequent_vlsm :=
48+
@Build_transition_item Sequent sequent_vlsm (existT I_V_IMP_RIGHT ()) (Some (seq [(A→B)→A] [A])) s0_seq (Some (seq [] [((A→B)→A)→A])).
49+
50+
Definition peirce_trace (A B : Formula) : list (transition_item sequent_vlsm) :=
51+
peirce_trace_pref A B ++ [peirce_trace_last A B].
52+
53+
Lemma s0_seq_initial :
54+
initial_state_prop sequent_vlsm s0_seq.
55+
Proof.
56+
unfold s0_seq.
57+
by destruct composite_s0.
58+
Qed.
59+
60+
Proposition valid_trans_peirce_1 :
61+
forall (A : Formula),
62+
input_valid_transition sequent_vlsm (existT I_V_ID A) (s0_seq, None) (s0_seq, Some (seq [A] [A])).
63+
Proof.
64+
intros A.
65+
repeat split.
66+
- apply initial_state_is_valid.
67+
exact s0_seq_initial.
68+
- apply option_valid_message_None.
69+
- by simpl; rewrite state_update_id.
70+
Qed.
71+
72+
Proposition valid_trans_peirce_2 :
73+
forall (A B : Formula),
74+
input_valid_transition sequent_vlsm (existT I_V_WK_RIGHT B) (s0_seq, Some (seq [A] [A])) (s0_seq, Some (seq [A] [B; A])).
75+
Proof.
76+
intros A B.
77+
repeat split.
78+
- apply initial_state_is_valid. exact s0_seq_initial.
79+
- app_valid_tran.
80+
exists (s0_seq, None). exists (existT I_V_ID A). exists s0_seq.
81+
exact (valid_trans_peirce_1 A).
82+
- simpl. rewrite state_update_id.
83+
+ reflexivity.
84+
+ auto.
85+
Qed.
86+
87+
Proposition valid_trans_peirce_3 :
88+
forall (A B : Formula),
89+
input_valid_transition sequent_vlsm (existT I_V_IMP_RIGHT ()) (s0_seq, Some (seq [A] [B; A])) (s0_seq, Some (seq [] [A→B; A])).
90+
Proof.
91+
intros A B.
92+
repeat split.
93+
- apply initial_state_is_valid. exact s0_seq_initial.
94+
- app_valid_tran.
95+
exists (s0_seq, Some (seq [A] [A])). exists (existT I_V_WK_RIGHT B). exists s0_seq.
96+
exact (valid_trans_peirce_2 A B).
97+
- simpl. rewrite state_update_id.
98+
+ reflexivity.
99+
+ auto.
100+
Qed.
101+
102+
Proposition valid_trans_peirce_4:
103+
forall (A : Formula),
104+
input_valid_transition sequent_vlsm (existT I_V_IMP_LEFT recLeft) (s0_seq, Some (seq [A] [A]))
105+
(state_update sequent_vlsm_components s0_seq I_V_IMP_LEFT (Some (seq [A] [A])), None).
106+
Proof.
107+
intros A.
108+
repeat split.
109+
- apply initial_state_is_valid. exact s0_seq_initial.
110+
- app_valid_tran.
111+
exists (s0_seq, None). exists (existT I_V_ID A). exists s0_seq.
112+
exact (valid_trans_peirce_1 A).
113+
Qed.
114+
115+
Proposition valid_trans_peirce_5:
116+
forall (A B : Formula),
117+
input_valid_transition sequent_vlsm (existT I_V_IMP_LEFT emitLeft)
118+
((state_update sequent_vlsm_components s0_seq I_V_IMP_LEFT (Some (seq [A] [A])) ), Some (seq [] [A→B; A]))
119+
(s0_seq, Some (seq [(A→B)→A] [A; A])).
120+
Proof.
121+
intros A B.
122+
repeat split.
123+
- exact (input_valid_transition_destination sequent_vlsm (valid_trans_peirce_4 A)).
124+
- exact (input_valid_transition_out sequent_vlsm (valid_trans_peirce_3 A B)).
125+
- simpl.
126+
by rewrite state_update_eq.
127+
- simpl.
128+
rewrite state_update_eq. rewrite state_update_twice.
129+
by rewrite state_update_id.
130+
Qed.
131+
132+
Proposition valid_trans_peirce_6:
133+
forall (A B : Formula),
134+
input_valid_transition sequent_vlsm (existT I_V_CT_RIGHT ())
135+
(s0_seq, Some (seq [(A→B)→A] [A; A])) (s0_seq, Some (seq [(A→B)→A] [A])).
136+
Proof.
137+
intros A B.
138+
repeat split.
139+
- apply initial_state_is_valid. exact s0_seq_initial.
140+
- exact (input_valid_transition_out sequent_vlsm (valid_trans_peirce_5 A B)).
141+
- simpl. destruct (decide (A = A)).
142+
+ subst. reflexivity.
143+
+ exfalso. apply n. reflexivity.
144+
- simpl.
145+
destruct (decide (A = A)); rewrite state_update_id.
146+
+ reflexivity.
147+
+ auto.
148+
+ exfalso. apply n. reflexivity.
149+
+ done.
150+
Qed.
151+
152+
Proposition valid_trans_peirce_7:
153+
forall (A B : Formula),
154+
input_valid_transition sequent_vlsm (existT I_V_IMP_RIGHT ())
155+
(s0_seq, Some (seq [(A→B)→A] [A])) (s0_seq, Some (seq [] [((A→B)→A)→A])).
156+
Proof.
157+
intros A B.
158+
repeat split.
159+
- apply initial_state_is_valid. exact s0_seq_initial.
160+
- exact (input_valid_transition_out sequent_vlsm (valid_trans_peirce_6 A B)).
161+
- simpl. rewrite state_update_id.
162+
+ reflexivity.
163+
+ auto.
164+
Qed.
165+
166+
Example peirce_trace_valid :
167+
forall (A B : Formula),
168+
finite_valid_trace_init_to sequent_vlsm s0_seq s0_seq (peirce_trace A B).
169+
Proof.
170+
intros A B.
171+
constructor; [| exact s0_seq_initial].
172+
repeat apply finite_valid_trace_from_to_extend.
173+
- apply finite_valid_trace_from_to_empty.
174+
apply initial_state_is_valid.
175+
exact s0_seq_initial.
176+
177+
- exact (valid_trans_peirce_7 A B).
178+
- exact (valid_trans_peirce_6 A B).
179+
- exact (valid_trans_peirce_5 A B).
180+
- exact (valid_trans_peirce_4 A).
181+
- exact (valid_trans_peirce_3 A B).
182+
- exact (valid_trans_peirce_2 A B).
183+
- exact (valid_trans_peirce_1 A).
184+
Qed.
185+
186+

‎src/Sequents.v‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,8 @@ Context
55

66
Module Export Form.
77

8+
(** * Formulas *)
9+
810
Inductive symbol : Type :=
911
| Top
1012
| Bot
@@ -48,10 +50,11 @@ Module Calculus.
4850
#[local] Notation "x ∧ y" := (FConj x y) (at level 80, right associativity).
4951
#[local] Notation "x → y" := (FImpl x y) (at level 99, y at level 200, right associativity).
5052

53+
(** * Sequents and Derivations *)
54+
5155
Inductive Sequent : Type :=
5256
| seq (Gamma Delta : list Formula) : Sequent.
5357

54-
5558
Inductive SC_derivation : nat -> Sequent -> Prop :=
5659
| SC_ID (A : Formula) : SC_derivation 0 (seq [A] [A])
5760
| SC_BOT : SC_derivation 0 (seq [⊥] [])
@@ -153,6 +156,8 @@ Inductive GK_derivation : nat -> Sequent -> Prop :=
153156
(Hd : GK_derivation h (seq Γ (Δ ++ A :: B :: Π))) :
154157
GK_derivation (S h) (seq Γ (Δ ++ B :: A :: Π)).
155158

159+
(** * Soundness with GK *)
160+
156161
Lemma SC_is_GK : forall (k : nat) (Γ Δ : list Formula),
157162
SC_derivation k (seq Γ Δ) ->
158163
exists (k' : nat), GK_derivation k' (seq Γ Δ).
@@ -212,6 +217,7 @@ Proof.
212217
exact (GK_XCHG_RIGHT _ _ _ _ _ _ H1).
213218
Qed.
214219

220+
(** * Completeness with GK *)
215221
Lemma GK_is_SC : forall (k : nat) (Γ Δ : list Formula),
216222
GK_derivation k (seq Γ Δ) ->
217223
exists (k' : nat), SC_derivation k' (seq Γ Δ).

0 commit comments

Comments
 (0)