Revision 58337f0d8889b1f231b6d6a1a789a27d8714c24c authored by Pierre-Yves Strub on 14 December 2015, 14:21:43 UTC, committed by Pierre-Yves Strub on 14 December 2015, 14:23:31 UTC
1 parent 7476fe1
IntExtra.ec
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2015 - IMDEA Software Institute
* Copyright (c) - 2012--2015 - Inria
*
* Distributed under the terms of the CeCILL-B-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
require import Option Int.
(* -------------------------------------------------------------------- *)
lemma lt0n n : (0 <= n) => (0 < n <=> n <> 0).
proof. by rewrite ltz_def => ->. qed.
lemma eqn0Ngt n : (0 <= n) => (n = 0) <=> !(0 < n).
proof. by rewrite eq_sym lez_eqVlt -ora_or => -[<-|?->]. qed.
lemma ltzS m n : (m < n+1) <=> (m <= n).
proof. by rewrite -lez_add1r addzC lez_add2r. qed.
lemma leqn0 n : 0 <= n => (n <= 0) <=> (n = 0).
proof. by rewrite eqz_leq => ->. qed.
lemma ltzE m n : (m < n) <=> (m+1 <= n).
proof. by rewrite -(ltz_add2r 1) ltzS. qed.
lemma ltz1 m : (m < 1) <=> (m <= 0).
proof. by rewrite -(ltzS m 0). qed.
lemma ltn1 m : 0 <= m => (m < 1) <=> (m = 0).
proof. by rewrite ltz1 eqz_leq => ->. qed.
(* -------------------------------------------------------------------- *)
op b2i (b : bool) = b ? 1 : 0.
lemma b2i0 : b2i false = 0. proof. by []. qed.
lemma b2i1 : b2i true = 1. proof. by []. qed.
lemma b2i_or b1 b2: b2i (b1 \/ b2) = b2i b1 + b2i b2 - b2i b1 * b2i b2.
proof. by rewrite /b2i; case: b1 b2 => [|] [|] //=; rewrite oppz0. qed.
lemma b2i_and b1 b2: b2i (b1 /\ b2) = b2i b1 * b2i b2.
proof. by rewrite /b2i; case: b1 b2 => [|] [|]. qed.
lemma le_b2i b1 b2: (b1 => b2) <=> (b2i b1 <= b2i b2).
proof. by case: b1 b2 => [|] [|]. qed.
lemma b2i_ge0 b: 0 <= b2i b.
proof. by case: b. qed.
lemma b2i_le1 b: b2i b <= 1.
proof. by case: b. qed.
lemma b2i_eq1 b : b2i b = 1 <=> b.
proof. by case: b. qed.
lemma b2i_eq0 b : b2i b = 0 <=> !b.
proof. by case: b. qed.
(* -------------------------------------------------------------------- *)
theory IterOp.
op iteri ['a] : int -> (int -> 'a -> 'a) -> 'a -> 'a.
axiom iteri0 ['a] n opr (x : 'a):
n <= 0 => iteri n opr x = x.
axiom iteriS ['a] n opr (x : 'a):
0 <= n => iteri (n+1) opr x = opr n (iteri n opr x).
lemma eq_iteri (f1 f2 : int -> 'a -> 'a) k a:
(forall i a, 0 <= i < k => f1 i a = f2 i a)
=> iteri k f1 a = iteri k f2 a.
proof.
elim/natind: k=> [n le0_n|n ge0_n ih] h; first by rewrite !iteri0.
rewrite !iteriS // h 1:ltz_addl ?ih // => i b [ge0_i lt_in].
by apply/h; rewrite ge0_i (ltz_trans n) // ltz_addl.
qed.
op iter ['a] n f x0 = iteri<:'a> n (fun i => f) x0.
lemma iter0 ['a] n opr (x : 'a): n <= 0 => iter n opr x = x.
proof. by move/iteri0<:'a>=> @/iter ->. qed.
lemma iterS ['a] n opr (x : 'a): 0 <= n =>
iter (n+1) opr x = opr (iter n opr x).
proof. by move/iteriS<:'a>=> @/iter ->. qed.
lemma iter1 ['a] opr (x : 'a): iter 1 opr x = opr x.
proof. by rewrite (@iterS 0) // iter0. qed.
lemma iter2 ['a] opr (x : 'a): iter 2 opr x = opr (opr x).
proof. by rewrite (@iterS 1) // iter1. qed.
lemma iterSr n opr (x : 'a):
0 <= n => iter (n + 1) opr x = iter n opr (opr x).
proof.
elim: n=> /=; first by rewrite (iterS 0) ?iter0.
by move=> n geo0 ih; rewrite iterS 2:ih ?iterS // addz_ge0.
qed.
op iterop ['a] (n : int) opr (x z : 'a) : 'a =
let f = fun i y, if i <= 0 then x else opr x y in
iteri n f z.
lemma iterop0 ['a] (n : int) opr (x z : 'a): n <= 0 =>
iterop n opr x z = z.
proof. by move=> le0_n; rewrite /iterop /= iteri0. qed.
lemma iterop1 ['a] opr (x z : 'a): iterop 1 opr x z = x.
proof. by rewrite /iterop /= (iteriS 0). qed.
lemma iteropS ['a] (n : int) opr (x z : 'a): 0 <= n =>
iterop (n+1) opr x z = iter n (opr x) x.
proof.
rewrite /iterop; elim: n=> /=; first by rewrite iter0 ?(iteriS 0).
move=> n ge0_n /= ih; rewrite iteriS 1:addz_ge0 //= ih.
by rewrite {1}addzC lez_add1r ltzNge ge0_n /= iterS.
qed.
end IterOp.
export IterOp.
(* -------------------------------------------------------------------- *)
op odd (z : int) = iter z [!] false.
lemma odd0 : !odd 0. proof. by rewrite iter0. qed.
lemma odd1 : odd 1. proof. by rewrite iter1. qed.
lemma odd2 : !odd 2. proof. by rewrite iter2. qed.
lemma oddS z : 0 <= z => odd (z + 1) = !(odd z).
proof. by move/iterS<:bool>=> ->. qed.
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...