-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathSoundness.v
75 lines (70 loc) · 3.6 KB
/
Soundness.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
Require Import Logic_and_Set_Theory.
From Coq Require Import Sets.Ensembles.
From Coq Require Import Sets.Powerset_facts.
From Coq Require Import Bool.
From Coq Require Import Constructive_sets.
Theorem Soundness: forall (Gamma:Ensemble Formula) (f:Formula) ,
ND Gamma f -> sfSf Gamma f.
Proof.
intros Gamma f H.
unfold sfSf.
intros model H1.
induction H.
+apply H1. apply H.
+apply IHND in H1. simpl in H1. apply andb_true_iff in H1. apply H1.
+apply IHND in H1. simpl in H1. apply andb_true_iff in H1. apply H1.
+assert (H2: mSsf model C). -apply H1. -apply IHND1 in H1. apply IHND2 in H2.
simpl. apply andb_true_iff. split. --apply H1. --apply H2.
+assert (H1':mSsf model C). -apply H1.
-apply IHND3 in H1. simpl in H1. apply orb_true_iff in H1. destruct H1.
--apply IHND1. unfold mSsf. intros f0. unfold mSsf in IHND1. unfold mSsf in H1'.
intros H3. apply Union_inv in H3. destruct H3. ---apply H1'. apply H3.
---apply Singleton_inv in H3. rewrite <- H3. apply H1.
--apply IHND2. unfold mSsf. intros f0. unfold mSsf in IHND1. unfold mSsf in H1'.
intros H3. apply Union_inv in H3. destruct H3. ---apply H1'. apply H3.
---apply Singleton_inv in H3. rewrite <- H3. apply H1.
+simpl. apply orb_true_iff. left. apply IHND. apply H1.
+simpl. apply orb_true_iff. right. apply IHND. apply H1.
+assert (H2:mSsf model C). -apply H1. -apply IHND1 in H1. apply IHND2 in H2.
simpl in H1. apply orb_true_iff in H1. destruct H1. apply negb_true_iff in H1.
--rewrite -> H1 in H2. discriminate. --apply H1.
+assert (forall b : bool, b=true \/ b=false).
-intros b. destruct b. --left. reflexivity. --right. reflexivity.
-assert (val model f1 = true \/ val model f1 = false).
--apply H0. --destruct H2.
---simpl. apply orb_true_iff. right. apply IHND.
unfold mSsf. intros f H3. apply Union_inv in H3.
destruct H3. ----apply H1. apply H3.
----apply Singleton_inv in H3. rewrite <- H3. apply H2.
---simpl. apply orb_true_iff. left. apply negb_true_iff. apply H2.
+simpl. assert (H2:mSsf model C). ++apply H1. ++apply IHND1 in H1. apply IHND2 in H2.
simpl in H2. rewrite -> H1 in H2. simpl in H2. apply H2.
+assert (mSsf model
(Union Formula C (Singleton Formula f)) -> False).
-intros H2. apply IHND in H2. simpl in H2. discriminate.
-assert (val model f = true -> False).
--intros H3. apply H0. unfold mSsf. intros f0 H4.
apply Union_inv in H4. destruct H4.
---apply H1 in H2. apply H2.
---apply Singleton_inv in H2. rewrite <- H2. apply H3.
--simpl. apply negb_true_iff. assert (forall b:bool, b=true \/ b=false).
---intros b. destruct b. ----left. reflexivity. ----right. reflexivity.
---assert (HL:val model f = true \/ val model f = false).
----apply H3. ----destruct HL.
-----apply H2 in H4. exfalso. apply H4.
-----apply H4.
+apply IHND in H1. simpl in H1. discriminate.
+assert (mSsf model
(Union Formula C (Singleton Formula (neg f))) -> False).
-intros H2. apply IHND in H2. simpl in H2. discriminate.
-assert (val model (neg f) = true -> False).
--intros H2. apply H0. unfold mSsf. intros f0 H3.
apply Union_inv in H3. destruct H3.
---apply H1. apply H3. ---apply Singleton_inv in H3. rewrite -> H3 in H2. apply H2.
--assert (forall b:bool, b=true \/ b=false).
---intros b. destruct b. ----left. reflexivity. ----right. reflexivity.
---assert (HL:val model (neg f) = true \/ val model (neg f) = false).
----apply H3. ----destruct HL.
-----apply H2 in H4. exfalso. apply H4. -----simpl in H4.
apply negb_false_iff in H4. apply H4.
Qed.