swh:1:snp:960b089228f647a5f611503985d0a438173f35bc
Tip revision: 9d08a76fb50773e0b6b1afad31f37dfb821fee75 authored by Benjamin Gregoire on 24 November 2022, 16:10:02 UTC
fix #154
fix #154
Tip revision: 9d08a76
CHoareTactic.ec
(* -------------------------------------------------------------------- *)
require import AllCore List Ring StdOrder StdBigop.
require (*--*) Bigop.
(*---*) import IntID IntOrder Bigint.
(* This lemma ensure the correctness of our rules for seq, wp ... *)
lemma subrK (x y : xint) : is_inf x \/ is_int y => (x - y) + y = x.
proof. case y => //; case x => //= *; ring. qed.
(* -------------------------------------------------------------------- *)
lemma add0x : left_id '0 xadd.
proof. by case. qed.
lemma addx0 : right_id '0 xadd.
proof. by case. qed.
hint simplify [reduce] add0x, addx0.
lemma addxA : associative xadd.
proof. by case=> [x|] [y|] [z|] => //=; rewrite addrA. qed.
lemma addxC : commutative xadd.
proof. by case=> [x|] [y|] => //=; rewrite addrC. qed.
(* -------------------------------------------------------------------- *)
lemma mul1x : left_id '1 xmul.
proof. by case. qed.
lemma mulx1 : right_id '1 xmul.
proof. by case. qed.
lemma mulxA : associative xmul.
proof. by case=> [x|] [y|] [z|] => //=; rewrite mulrA. qed.
lemma mulxC : commutative xmul.
proof. by case=> [x|] [y|] => //=; rewrite mulrC. qed.
(* -------------------------------------------------------------------- *)
lemma xaddInfx (x:xint) : Inf + x = Inf.
proof. by case: x. qed.
lemma xaddxInf (x:xint) : x + Inf = Inf.
proof. by case: x. qed.
lemma xmulInfx (x:xint) : Inf * x = Inf.
proof. by case: x. qed.
lemma xmulxInf (x:xint) : x * Inf = Inf.
proof. by case: x. qed.
hint simplify xaddInfx, xaddxInf, xmulInfx, xmulxInf.
(* -------------------------------------------------------------------- *)
op xle (x y : xint) =
with x = N x, y = N y => (x <= y)
with x = N x, y = Inf => true
with x = Inf, y = N y => false
with x = Inf, y = Inf => true.
abbrev (<=) = xle.
lemma lexx : reflexive (<=).
proof. by case. qed.
lemma lexx_rw (x y : xint) : x = y => x <= y.
proof. by move=> ->; apply lexx. qed.
hint simplify lexx_rw.
lemma lex_anti (x y : xint) : x <= y <= x => x = y.
proof. by case: x y => [x|] [y|] //=; apply: ler_anti. qed.
lemma lex_trans : transitive (<=).
proof. by case=> [x|] [y|] [z|] //=; apply: ler_trans. qed.
lemma lex_inf (x : xint) : x <= Inf.
proof. by case: x. qed.
lemma lex_add2r (x1 x2 y : xint) :
x1 <= x2 => x1 + y <= x2 + y.
proof.
by case: x1 x2 y => [x1|] [x2|] [y|] //=; apply: ler_add2r.
qed.
lemma is_int_le x y : x <= y => is_int y => is_int x.
proof. by case: x => //; case: y. qed.
lemma lex_add2l (x1 x2 y : xint) :
x1 <= x2 => y + x1 <= y + x2.
proof. by rewrite !(@addxC y) &(lex_add2r). qed.
op xmax (x y : xint) =
with x = N x, y = N y => N (max x y)
with x = N _, y = Inf => Inf
with x = Inf, y = N _ => Inf
with x = Inf, y = Inf => Inf.
lemma sub_completness (t1 t2 t:xint) :
t1 + t2 <= t <=>
t1 <= t - t2 /\ (is_int t2 \/ is_inf t).
proof.
case: t t1 t2 => [i | ] [i1 | ] [i2 | ] //=; smt().
qed.
(* -------------------------------------------------------------------- *)
theory Bigxint.
clone include Bigop
with type t <- xint,
op Support.idm <- ('0),
op Support.(+) <- xadd
proof *.
realize Support.Axioms.addmA by exact/addxA.
realize Support.Axioms.addmC by exact/addxC.
realize Support.Axioms.add0m by exact/add0x.
lemma nosmt big_morph_N (P : 'a -> bool) (f : 'a -> int) s:
big P (fun i => N (f i)) s = N (BIA.big P (fun i => f i) s).
proof.
elim: s => [|x s ih] //=.
by rewrite !(big_cons, BIA.big_cons) ih /=; case: (P x).
qed.
lemma nosmt big_const_Nx (P : 'a -> bool) x s:
big P (fun _ => N x) s = (count P s) ** N x.
proof. by rewrite big_morph_N /= big_constz mulrC. qed.
lemma nosmt big_constx (P : 'a -> bool) x s: x <> Inf =>
big P (fun _ => x) s = (count P s) ** x.
proof. by case: x => //= x; apply: big_const_Nx. qed.
lemma big_constNz x (s: 'a list) :
big predT (fun _ => N x) s = N (size s * x).
proof. by rewrite big_const_Nx count_predT. qed.
lemma bigi_constz x (n m:int) :
n <= m =>
bigi predT (fun _ => N x) n m = N ((m - n) * x).
proof. by move=> hnm;rewrite big_constNz size_range /#. qed.
end Bigxint.
export Bigxint.
(* ------------------------------------------------------------------------------ *)
lemma is_int_xopp (x:xint) : is_int x => is_int (-x).
proof. by case: x. qed.
lemma is_int_xadd (x y: xint) :
is_int x => is_int y => is_int (x + y).
proof. by case: x; case y. qed.
lemma is_int_xmul (x y: xint) :
is_int x => is_int y => is_int (x * y).
proof. by case: x; case y. qed.
hint simplify is_int_xopp, is_int_xadd, is_int_xmul.
lemma is_int_big (P: 'a -> bool) (f:'a -> xint) (s:'a list) :
(forall x, is_int (f x)) =>
is_int (big P f s).
proof.
move=> h; elim: s.
+ by rewrite big_nil.
move=> x l hl; rewrite big_cons; case: (P x) => ? //.
by apply is_int_xadd => //; apply h.
qed.
hint simplify is_int_big.
(* -------------------------------------------------------------------- *)
lemma N_D (x y : int) : N (x + y) = N x + N y.
proof. by []. qed.
lemma N_N (x : int) : N (-x) = -N x.
proof. by []. qed.
lemma N_B (x y : int) : N (x-y) = N x - N y.
proof. by []. qed.
lemma mono_N_le (x y : int): x <= y <=> N x <= N y.
proof. by []. qed.