imp_n_Imp_consequence_rule_1.v 6.76 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
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 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
Require Import ZArith.
Require Import Rbase.
Parameter ident : Type.

Axiom ident_eq_dec : forall (i1:ident) (i2:ident), (i1 = i2) \/ ~ (i1 = i2).

Parameter mk_ident: Z -> ident.


Axiom mk_ident_inj : forall (i:Z) (j:Z), ((mk_ident i) = (mk_ident j)) ->
  (i = j).

Inductive operator  :=
  | Oplus : operator 
  | Ominus : operator 
  | Omult : operator .

Inductive expr  :=
  | Econst : Z -> expr 
  | Evar : ident -> expr 
  | Ebin : expr -> operator -> expr -> expr .

Inductive stmt  :=
  | Sskip : stmt 
  | Sassign : ident -> expr -> stmt 
  | Sseq : stmt -> stmt -> stmt 
  | Sif : expr -> stmt -> stmt -> stmt 
  | Swhile : expr -> stmt -> stmt .

Axiom check_skip : forall (s:stmt), (s = Sskip) \/ ~ (s = Sskip).

Parameter map : forall (a:Type) (b:Type), Type.

Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.

Implicit Arguments get.

Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).

Implicit Arguments set.

Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
  forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
  a2) = b1).

Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
  forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
  a2) = (get m a2)).

Parameter const: forall (b:Type) (a:Type), b -> (map a b).

Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.

Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
  b1):(map a b)) a1) = b1).

Definition state  := (map ident Z).

Definition eval_bin(x:Z) (op:operator) (y:Z): Z :=
  match op with
  | Oplus => (x + y)%Z
  | Ominus => (x - y)%Z
  | Omult => (x * y)%Z
  end.

Set Implicit Arguments.
Fixpoint eval_expr(s:(map ident Z)) (e:expr) {struct e}: Z :=
  match e with
  | (Econst n) => n
  | (Evar x) => (get s x)
  | (Ebin e1 op e2) => (eval_bin (eval_expr s e1) op (eval_expr s e2))
  end.
Unset Implicit Arguments.

Inductive one_step : (map ident Z) -> stmt -> (map ident Z)
  -> stmt -> Prop :=
  | one_step_assign : forall (s:(map ident Z)) (x:ident) (e:expr),
      (one_step s (Sassign x e) (set s x (eval_expr s e)) Sskip)
  | one_step_seq : forall (s:(map ident Z)) (sqt:(map ident Z)) (i1:stmt)
      (i1qt:stmt) (i2:stmt), (one_step s i1 sqt i1qt) -> (one_step s (Sseq i1
      i2) sqt (Sseq i1qt i2))
  | one_step_seq_skip : forall (s:(map ident Z)) (i:stmt), (one_step s
      (Sseq Sskip i) s i)
  | one_step_if_true : forall (s:(map ident Z)) (e:expr) (i1:stmt) (i2:stmt),
      (~ ((eval_expr s e) = 0%Z)) -> (one_step s (Sif e i1 i2) s i1)
  | one_step_if_false : forall (s:(map ident Z)) (e:expr) (i1:stmt)
      (i2:stmt), ((eval_expr s e) = 0%Z) -> (one_step s (Sif e i1 i2) s i2)
  | one_step_while_true : forall (s:(map ident Z)) (e:expr) (i:stmt),
      (~ ((eval_expr s e) = 0%Z)) -> (one_step s (Swhile e i) s (Sseq i
      (Swhile e i)))
  | one_step_while_false : forall (s:(map ident Z)) (e:expr) (i:stmt),
      ((eval_expr s e) = 0%Z) -> (one_step s (Swhile e i) s Sskip).

Axiom progress : forall (s:(map ident Z)) (i:stmt), (~ (i = Sskip)) ->
  exists sqt:(map ident Z), exists iqt:stmt, (one_step s i sqt iqt).

Inductive many_steps : (map ident Z) -> stmt -> (map ident Z) -> stmt
  -> Z -> Prop :=
  | many_steps_refl : forall (s:(map ident Z)) (i:stmt), (many_steps s i s i
      0%Z)
  | many_steps_trans : forall (s1:(map ident Z)) (s2:(map ident Z)) (s3:(map
      ident Z)) (i1:stmt) (i2:stmt) (i3:stmt) (n:Z), (one_step s1 i1 s2
      i2) -> ((many_steps s2 i2 s3 i3 n) -> (many_steps s1 i1 s3 i3
      (n + 1%Z)%Z)).

Axiom steps_non_neg : forall (s1:(map ident Z)) (s2:(map ident Z)) (i1:stmt)
  (i2:stmt) (n:Z), (many_steps s1 i1 s2 i2 n) -> (0%Z <= n)%Z.

Axiom many_steps_seq : forall (s1:(map ident Z)) (s3:(map ident Z)) (i1:stmt)
  (i2:stmt) (n:Z), (many_steps s1 (Sseq i1 i2) s3 Sskip n) -> exists s2:(map
  ident Z), exists n1:Z, exists n2:Z, (many_steps s1 i1 s2 Sskip n1) /\
  ((many_steps s2 i2 s3 Sskip n2) /\ (n = ((1%Z + n1)%Z + n2)%Z)).

Inductive fmla  :=
  | Fterm : expr -> fmla 
  | Fand : fmla -> fmla -> fmla 
  | Fnot : fmla -> fmla 
  | Fimplies : fmla -> fmla -> fmla .

Set Implicit Arguments.
Fixpoint eval_fmla(s:(map ident Z)) (f:fmla) {struct f}: Prop :=
  match f with
  | (Fterm e) => ~ ((eval_expr s e) = 0%Z)
  | (Fand f1 f2) => (eval_fmla s f1) /\ (eval_fmla s f2)
  | (Fnot f1) => ~ (eval_fmla s f1)
  | (Fimplies f1 f2) => (eval_fmla s f1) -> (eval_fmla s f2)
  end.
Unset Implicit Arguments.

Parameter subst_expr: expr -> ident -> expr -> expr.


Axiom subst_expr_def : forall (e:expr) (x:ident) (t:expr),
  match e with
  | (Econst _) => ((subst_expr e x t) = e)
  | (Evar y) => ((x = y) -> ((subst_expr e x t) = t)) /\ ((~ (x = y)) ->
      ((subst_expr e x t) = e))
  | (Ebin e1 op e2) => ((subst_expr e x t) = (Ebin (subst_expr e1 x t) op
      (subst_expr e2 x t)))
  end.

Axiom eval_subst_expr : forall (s:(map ident Z)) (e:expr) (x:ident) (t:expr),
  ((eval_expr s (subst_expr e x t)) = (eval_expr (set s x (eval_expr s t))
  e)).

Set Implicit Arguments.
Fixpoint subst(f:fmla) (x:ident) (t:expr) {struct f}: fmla :=
  match f with
  | (Fterm e) => (Fterm (subst_expr e x t))
  | (Fand f1 f2) => (Fand (subst f1 x t) (subst f2 x t))
  | (Fnot f1) => (Fnot (subst f1 x t))
  | (Fimplies f1 f2) => (Fimplies (subst f1 x t) (subst f2 x t))
  end.
Unset Implicit Arguments.

Axiom eval_subst : forall (s:(map ident Z)) (f:fmla) (x:ident) (t:expr),
  (eval_fmla s (subst f x t)) <-> (eval_fmla (set s x (eval_expr s t)) f).

Definition valid_fmla(p:fmla): Prop := forall (s:(map ident Z)), (eval_fmla s
  p).

Definition valid_triple(p:fmla) (i:stmt) (q:fmla): Prop := forall (s:(map
  ident Z)), (eval_fmla s p) -> forall (sqt:(map ident Z)) (n:Z),
  (many_steps s i sqt Sskip n) -> (eval_fmla sqt q).

Axiom skip_rule : forall (q:fmla), (valid_triple q Sskip q).

Axiom assign_rule : forall (q:fmla) (x:ident) (e:expr),
  (valid_triple (subst q x e) (Sassign x e) q).

Axiom seq_rule : forall (p:fmla) (q:fmla) (r:fmla) (i1:stmt) (i2:stmt),
  ((valid_triple p i1 r) /\ (valid_triple r i2 q)) -> (valid_triple p
  (Sseq i1 i2) q).

Axiom if_rule : forall (e:expr) (p:fmla) (q:fmla) (i1:stmt) (i2:stmt),
  ((valid_triple (Fand p (Fterm e)) i1 q) /\ (valid_triple (Fand p
  (Fnot (Fterm e))) i2 q)) -> (valid_triple p (Sif e i1 i2) q).

Axiom while_rule : forall (e:expr) (inv:fmla) (i:stmt),
  (valid_triple (Fand (Fterm e) inv) i inv) -> (valid_triple inv (Swhile e i)
  (Fand (Fnot (Fterm e)) inv)).

(* YOU MAY EDIT THE CONTEXT BELOW *)

(* DO NOT EDIT BELOW *)

Theorem consequence_rule : forall (p:fmla) (pqt:fmla) (q:fmla) (qqt:fmla)
  (i:stmt), (valid_triple p i q) -> (valid_triple pqt i qqt).
(* YOU MAY EDIT THE PROOF BELOW *)
intros p p' q q' i H.

Qed.
(* DO NOT EDIT BELOW *)