https://github.com/EasyCrypt/easycrypt
Tip revision: c997f51867b38bef59be4292a60ac0119a3714a1 authored by Pierre-Yves Strub on 12 September 2018, 11:42:14 UTC
fix parsing of codeposition
fix parsing of codeposition
Tip revision: c997f51
Core.ec
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-B-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
lemma nosmt pw_eq ['a 'b] (x x' : 'a) (y y' : 'b):
x = x' => y = y' => (x, y) = (x', y').
proof. by move=> -> ->. qed.
lemma nosmt pairS (x : 'a * 'b): x = (fst x, snd x).
proof. by case: x. qed.
lemma nosmt fst_pair ['a 'b] (x : 'a) (y : 'b) : fst (x, y) = x by done.
lemma nosmt snd_pair ['a 'b] (x : 'a) (y : 'b) : snd (x, y) = y by done.
(* -------------------------------------------------------------------- *)
lemma nosmt oget_none: oget None<:'a> = witness.
proof. by done. qed.
lemma nosmt oget_some (x : 'a): oget (Some x) = x.
proof. by done. qed.
lemma nosmt some_oget (x : 'a option): x <> None => x = Some (oget x).
proof. by case: x. qed.
lemma nosmt someI (x y:'a): Some x = Some y => x = y.
proof. by done. qed.
lemma nosmt none_omap ['a 'b] (f : 'a -> 'b) ox :
omap f ox = None <=> ox = None.
proof. by case: ox. qed.
lemma oget_omap_some ['a 'b] (f : 'a -> 'b) ox :
ox <> None => oget (omap f ox) = f (oget ox).
proof. by case: ox. qed.
(* -------------------------------------------------------------------- *)
lemma nosmt frefl (f : 'a -> 'b): f == f by [].
lemma nosmt fsym (f g : 'a -> 'b): f == g => g == f by [].
lemma nosmt ftrans (f g h : 'a -> 'b): f == g => g == h => f == h by [].
(* -------------------------------------------------------------------- *)
lemma econgr1 ['a 'b] (f g : 'a -> 'b) x y: f == g => x = y => f x = g y.
proof. by move/fun_ext=> -> ->. qed.
(* -------------------------------------------------------------------- *)
lemma nosmt f2refl (f : 'a -> 'b -> 'c): f === f by [].
lemma nosmt f2sym (f g : 'a -> 'b -> 'c): f === g => g === f by [].
lemma nosmt f2trans (f g h : 'a -> 'b -> 'c): f === g => g === h => f === h by [].
lemma rel_ext (f g : 'a -> 'b -> 'c) : f = g <=> f === g.
proof.
by split=> //= fg; apply/fun_ext=> x; apply/fun_ext=> y; rewrite fg.
qed.
(* -------------------------------------------------------------------- *)
lemma eqL (x:'a): (fun y => x = y) = (=) x.
proof. by apply fun_ext. qed.
lemma eqR (y:'a): (fun x => x = y) = (=) y.
proof. by apply fun_ext=> x; rewrite (eq_sym x). qed.
(* -------------------------------------------------------------------- *)
lemma nosmt etaP (f : 'a -> 'b): eta_ f = f.
proof. by apply/fun_ext; rewrite etaE. qed.
(* -------------------------------------------------------------------- *)
lemma comp_eqE ['a 'b 'c] (f f' : 'b -> 'a) (g g' : 'c -> 'b):
f == f' => g == g' => (f \o g) == (f' \o g').
proof. by do 2! (move/fun_ext=> ->). qed.
(* -------------------------------------------------------------------- *)
lemma nosmt can_pcan (f:'a -> 'b) g: cancel f g => pcancel f (Some \o g).
proof. by move=> fK x; rewrite /(\o) fK. qed.
lemma nosmt pcan_inj (f:'a -> 'b) g: pcancel f g => injective f.
proof. by move=> fK x y /(congr1 g); rewrite !fK. qed.
lemma nosmt can_inj (f : 'a -> 'b) g: cancel f g => injective f.
proof. by move/can_pcan/pcan_inj. qed.
lemma nosmt canLR (f:'a -> 'b) g x y: cancel f g => x = f y => g x = y.
proof. by move=> fK ->; rewrite fK. qed.
lemma nosmt canRL (f:'a -> 'b) g x y: cancel f g => f x = y => x = g y.
proof. by move=> fK <-; rewrite fK. qed.
lemma nosmt inj_eq (f : 'a -> 'b):
injective f => forall x y, (f x = f y) <=> (x = y).
proof. by move=> inj_f x y; split=> [| -> //]; apply inj_f. qed.
lemma nosmt can_eq (f : 'a -> 'b) g:
cancel f g => forall x y, (f x = f y) <=> (x = y).
proof. by move=> can_fg; apply inj_eq; apply (can_inj f g). qed.
lemma nosmt can2_eq (f : 'a -> 'b) g:
cancel f g => cancel g f => forall x y, (f x = y) <=> (x = g y).
proof. by move=> fK gK x y; rewrite -{1}gK; apply (can_eq f g). qed.
(* -------------------------------------------------------------------- *)
lemma nosmt inj_idfun: injective (idfun<:'a>).
proof. by []. qed.
lemma nosmt inj_can_sym (f:'a -> 'b) f':
cancel f f' => injective f' => cancel f' f.
proof. by move=> fK injf' x; apply injf'; rewrite fK. qed.
lemma nosmt inj_comp (f:'b -> 'a) (h:'c -> 'b):
injective f => injective h => injective (f \o h).
proof. by move=> injf injh x y /injf /injh. qed.
lemma nosmt can_comp (f:'b -> 'a) (h:'c -> 'b) f' h':
cancel f f' => cancel h h' => cancel (f \o h) (h' \o f').
proof. by move=> fK hK x; rewrite /(\o) fK hK. qed.
lemma nosmt pcan_pcomp (f:'b -> 'a) (h:'c -> 'b) f' h':
pcancel f f' => pcancel h h' => pcancel (f \o h) (h' \c f').
proof. by move=> fK hK x; rewrite /(\o) /(\c) fK /= hK. qed.
lemma nosmt eq_inj (f g:'a -> 'b):
injective f => f == g => injective g.
proof. by move=> injf eqfg x y; rewrite -2!eqfg; apply injf. qed.
lemma nosmt eq_can (f g:'a -> 'b) f' g':
cancel f f' => f == g => f' == g' => cancel g g'.
proof. by move=> fK eqfg eqfg' x; rewrite -eqfg -eqfg' fK. qed.
lemma nosmt inj_can_eq (f g:'a -> 'b) f':
cancel f f' => injective f' => cancel g f' => f == g.
proof. by move=> fK injf' gK x; apply injf'; rewrite fK gK. qed.
(* -------------------------------------------------------------------- *)
lemma nosmt bij_inj (f:'b -> 'a): bijective f => injective f.
proof. by case=> g [fK _]; apply (can_inj f g). qed.
lemma nosmt bij_can_sym (f:'b -> 'a) f':
bijective f => (cancel f' f <=> cancel f f').
proof.
move=> bij_f; have /bij_inj inj_f := bij_f.
split=> fK; 1: by apply/inj_can_sym.
by case: bij_f=> h [_ hK] x; rewrite -hK fK.
qed.
lemma nosmt bij_can_eq (f:'b -> 'a) f' f'':
bijective f => cancel f f' => cancel f f'' => f' == f''.
proof.
move=> big_j fK fK'; apply/(inj_can_eq _ _ f);
by rewrite 1?bij_can_sym //; apply/bij_inj.
qed.
(* -------------------------------------------------------------------- *)
lemma nosmt eq_bij (f:'b -> 'a):
bijective f => forall g, f == g => bijective g.
proof.
case=> f' [fK f'K] g eqfg; exists f'; split.
by apply (eq_can f _ f'). by apply (eq_can f' _ f).
qed.
lemma nosmt bij_comp (f:'b -> 'a) (h:'c -> 'b):
bijective f => bijective h => bijective (f \o h).
proof.
move=> [f' [fK f'K]] [h' [hK h'K]].
by exists (h' \o f'); split; apply can_comp.
qed.
lemma nosmt bij_can_bij (f:'b -> 'a):
bijective f => forall f', cancel f f' => bijective f'.
proof. by move=> bij_f f' can_ff'; exists f; rewrite bij_can_sym. qed.
(* -------------------------------------------------------------------- *)
lemma nosmt inv_inj (f:'a -> 'a): involutive f => injective f.
proof. by apply can_inj. qed.
lemma nosmt inv_bij (f:'a -> 'a): involutive f => bijective f.
proof. by move=> invf; exists f. qed.
lemma nosmt inv_eq ['a] (f : 'a -> 'a) :
involutive f => forall x y, (f x = y) <=> (x = f y).
proof. by move=> fK; apply/can2_eq. qed.
(* -------------------------------------------------------------------- *)
(* Any extensional equality can be used to rewrite *)
lemma ext_rewrite (ext : 'a -> 'a -> bool) (a1 a2 : 'a) P:
(forall x y, ext x y => x = y) => ext a1 a2 => P a1 <=> P a2.
proof. by move=> ext_eq /ext_eq ->. qed.
(* -------------------------------------------------------------------- *)
lemma pred_ext (P Q : 'a -> bool):
P = Q <=> forall x, P x <=> Q x.
proof. by split=> //= h; apply/fun_ext=> x; rewrite h. qed.
(* -------------------------------------------------------------------- *)
pred (<=) (p q:'a -> bool) = (* subpred *)
forall a, p a => q a.
pred (< ) (p q:'a -> bool) = (* proper *)
p <= q /\ !(q <= p).
(* -------------------------------------------------------------------- *)
lemma nosmt subpred_eqP (p1 p2 : 'a -> bool):
(forall x, p1 x <=> p2 x) <=> (p1 <= p2 /\ p2 <= p1)
by [].
lemma nosmt subpred_refl (X : 'a -> bool): X <= X
by [].
lemma nosmt subpred_asym (X Y:'a -> bool):
X <= Y => Y <= X => X = Y
by (rewrite fun_ext; smt).
lemma nosmt subpred_trans (X Y Z:'a -> bool):
X <= Y => Y <= Z => X <= Z
by [].
(* -------------------------------------------------------------------- *)
lemma nosmt pred1E (c : 'a) : pred1 c = ((=) c).
proof. by apply fun_ext=> x; rewrite (eq_sym c). qed.
lemma nosmt predU1l (x y : 'a) b : x = y => (x = y) \/ b by [].
lemma nosmt predU1r (x y : 'a) b : b => (x = y) \/ b by [].
lemma nosmt eqVneq (x y : 'a) : x = y \/ x <> y by [].
lemma nosmt predT_comp ['a 'b] (p : 'a -> 'b) : predT \o p = predT.
proof. by []. qed.
lemma nosmt predIC (p1 p2 : 'a -> bool) : predI p1 p2 = predI p2 p1.
proof. by apply fun_ext=> x; rewrite /predI andbC. qed.
lemma nosmt predCI (p : 'a -> bool) : predI (predC p) p = pred0.
proof. by apply/fun_ext=> x /=; case: (p x); delta=> ->. qed. (* delta *)
lemma nosmt predCU (p : 'a -> bool) : predU (predC p) p = predT.
proof. by apply fun_ext=> x /=; case (p x); delta=> ->. qed. (* delta *)
lemma nosmt subpredUl (p1 p2 : 'a -> bool):
p1 <= predU p1 p2
by [].
lemma nosmt subpredUr (p1 p2 : 'a -> bool):
p2 <= predU p1 p2
by [].
lemma nosmt predIsubpredl (p1 p2 : 'a -> bool):
predI p1 p2 <= p1
by [].
lemma nosmt predIsubpredr (p1 p2 : 'a -> bool):
predI p1 p2 <= p2
by [].
lemma nosmt predTofV (f : 'a -> 'b): predT \o f = predT.
proof. by apply/fun_ext=> x. qed.