outcome-logic-coq/theories/lemmas.v at main · InnovativeInventor/outcome-logic-coq · GitHub

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
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
Require Import assertion.
Require Import semantics.
Require Import set.
Require Import ol.
Require Import util.

Ltac simp' :=
  match goal with
  | [ H : _ ∈ (fun _ => (𝟙, _) ⇓ _) |- _ ] =>
      inversion H; clear H
  | [ H : _ ∈ (fun _ => (_ ⨟ (_ ⋆), _) ⇓ _) |- _ ] =>
      idtac
  | [ H : _ ∈ (fun _ => (_ ⨟ _, _) ⇓ _) |- _ ] =>
      inversion H; clear H
  | [ H : _ ∈ (fun _ => (_ + _, _) ⇓ _) |- _ ] =>
      inversion H; clear H
  | [ H : _ ∈ (fun _ => (_ ⋆, _) ⇓ _) |- _ ] =>
      inversion H; clear H
  | [ H : _ ∈ (fun _ => (Atom _, _) ⇓ _) |- _ ] =>
      inversion H; clear H
  | [ H : (𝟙, _) ⇓ _ |- _ ] =>
      inversion H; clear H
  | [ H : (_ ⨟ (_ ⋆), _) ⇓ _ |- _ ] =>
      idtac
  | [ H : (_ ⨟ _, _) ⇓ _ |- _ ] =>
      inversion H; clear H
  | [ H : (_ + _, _) ⇓ _ |- _ ] =>
      inversion H; clear H
  | [ H : (_ ⋆, _) ⇓ _ |- _ ] =>
      inversion H; clear H
  | [ H : (Atom _, _) ⇓ _ |- _ ] =>
      inversion H; clear H
  | [ H : eval_cmd (Assume _) _ _ |- _ ] =>
      inversion H; clear H
  | [ H : eval_cmd (¬ _) _ _ |- _ ] =>
      inversion H; clear H
  | [ H : eval_cmd (_ <- alloc) _ _ |- _ ] =>
      inversion H; clear H
  | [ H : eval_cmd (_ <- _) _ _ |- _ ] =>
      inversion H; clear H
  | [ H : eval_cmd ([ _ ] <- _) _ _ |- _ ] =>
      inversion H; clear H
  | [ H : eval_cmd (_ <- [ _ ]) _ _ |- _ ] =>
      inversion H; clear H
  | [ H : <{ _ , _ }> = <{ _ , _ }> |- _ ] =>
      inversion H; clear H
  | _ => simp
  end.

Ltac simpgoal' :=
  repeat (unfold bind, outputs, triple, ret in *; simpl in *; simp').

Lemma eq_set_respects_sat_atom S S' P :
  S ≡ S' ->
  S ⊨atom P ->
  S' ⊨atom P.
Proof.
  revert S S'. induction P; simpl in *; intros; simpgoal.
  - repeat eexists; try eassumption.
    + intros Hin. apply H1. apply H. apply Hin.
    + intros Hin. apply H. apply H1. apply Hin.
  - repeat eexists.
    + intros Hin. apply H0. apply H. apply Hin.
    + intros Hin. apply H. apply H0. apply Hin.
Qed.

Lemma eq_set_respects_sat S S' phi :
  S ≡ S' ->
  S ⊨ phi ->
  S' ⊨ phi.
Proof.
  revert S S'. induction phi; intros S S' Heq Hsat; simpgoal; eauto.
  - intros ?. split; intros. specialize (Heq x).
    specialize (Hsat x). simpgoal. solve_eq_set.
  - repeat eexists; intros; try eassumption.
    + apply H. apply Heq. assumption.
    + unfold "◇" in *. simpgoal.
      * solve_eq_set. apply Heq. apply H. left. assumption.
      * solve_eq_set. apply Heq. apply H. right. assumption.
  - apply Hsat; eauto with sets.
  - eapply eq_set_respects_sat_atom; eauto.
Qed.

Lemma null_implies_unmapped x S : S ⊨ x == null ⇒ x -/->.
Proof.
  intros S' Heq [σ [Hin Hsat]]. unfold sat, sat_atom, sat_state in *.
  exists σ. split.
  - simpgoal'. repeat eexists. eauto.
  - simpgoal'. repeat eexists.
    + intros Hin. apply Hsat. apply Hin.
    + intros Hin. apply Hsat. apply Hin.
Qed.

Lemma syntactic_to_semantic_triples_neg phi C psi phi_sem psi_sem :
  (phi_sem = semantic_interpretation phi /\
      psi_sem = semantic_interpretation psi) ->
  ((⊭sem ⟨ phi_sem ⟩ C ⟨ psi_sem ⟩) <-> (⊭ ⟨ phi ⟩ C ⟨ psi ⟩)).
Proof.
  intros.
  split.
  * destruct H. intros.
    unfold semantic_triple_neg in *.
    unfold triple_neg in *.
    destruct H1.
    exists x.
    destruct H1.
    subst.
    unfold semantic_interpretation in *.
    split; auto.
  * destruct H. intros.
    unfold semantic_triple_neg in *.
    unfold triple_neg in *.
    destruct H1.
    exists x.
    destruct H1.
    subst.
    unfold semantic_interpretation in *.
    split; auto.
Defined.

Lemma syntactic_to_semantic_triples_ext phi C psi phi_sem psi_sem :
  ((phi_sem ≡ (semantic_interpretation phi)) /\
      (psi_sem ≡ (semantic_interpretation psi))) ->
  ((⊨sem ⟨ phi_sem ⟩ C ⟨ psi_sem ⟩) <-> (⊨ ⟨ phi ⟩ C ⟨ psi ⟩)).
Proof.
  split.
  * destruct H. intros.
    unfold semantic_triple in *.
    unfold triple in *.
    intros.
    specialize (H1 S).
    unfold eq_set in *.
    assert (S ∈ phi_sem).
    {
      unfold member.
      eapply H.
      unfold semantic_interpretation.
      apply H2.
    }
    specialize (H1 H3).
    unfold member in H1.
    erewrite H0 in H1.
    unfold semantic_interpretation in H1.
    apply H1.
  * intros.
    destruct H.
    unfold semantic_triple.
    intros.
    subst.
    unfold triple in H0.
    unfold eq_set in *.
    specialize (H0 m).
    unfold member in *.
    erewrite H1.
    erewrite H in H2.
    unfold semantic_interpretation in *.
    apply H0.
    apply H2.
Qed.
(* the above few proofs can probably be simplified *)