https://github.com/EasyCrypt/easycrypt
Tip revision: a79f9aeb6de046ca12210d26317fab59c175d0dd authored by Pierre-Yves Strub on 08 July 2014, 09:43:21 UTC
Fix bug w.r.t. _tools presence detection.
Fix bug w.r.t. _tools presence detection.
Tip revision: a79f9ae
Fun.ec
(* --------------------------------------------------------------------
* Copyright IMDEA Software Institute / INRIA - 2013, 2014
* -------------------------------------------------------------------- *)
(* Parts of this API have been imported from the [seq] library of
* the ssreflect library that is (c) Copyright Microsoft Corporation
* and Inria. *)
require import ExtEq.
require import Option.
(*** Properties of functions (see ssrfun) *)
(** Definitions *)
(* id<:'a> is the identity function on 'a *)
op id (x:'a) = x.
(* preim f p x <=> x is in the preimage of p by f *)
pred preim ['a 'b] (f : 'a -> 'b) p x = p (f x).
(** Definitions for composition *)
theory Composition.
op comp (g:'b -> 'c) (f:'a -> 'b): ('a -> 'c) =
fun x, g (f x).
op pcomp (f:'b -> 'a option) (g:'c -> 'b option) x =
obind f (g x).
lemma eq_comp (f:'b -> 'a) f' (g:'c -> 'b) g':
f == f' =>
g == g' =>
comp f g == comp f' g'.
proof. by move=> eq_ff' eq_gg' x; rewrite /comp eq_gg' eq_ff'. qed.
end Composition.
export Composition.
theory Morphism.
(** Morphisms *)
(* Morphism property for unary and binary functions *)
pred morphism_1 (f:'a -> 'b) aF rF =
forall x, f (aF x) = rF (f x).
pred morphism_2 (f:'a -> 'b) aOp rOp =
forall x y, f (aOp x y) = rOp (f x) (f y).
(* Homomorphism property for unary and binary relations *)
pred homomorphism_1 (f:'a -> 'b) aP rP =
forall x, aP x => rP (f x).
pred homomorphism_2 (f:'a -> 'b) aR rR =
forall x y, aR x y => rR (f x) (f y).
(* Stability property for unary and binary relations *)
pred monomorphism_1 (f:'a -> 'b) (aP: 'a -> 'c) rP =
forall x, rP (f x) = aP x.
pred monomorphism_2 (f:'a -> 'b) (aR:'a -> 'a -> 'c) rR =
forall x y, rR (f x) (f y) = aR x y.
end Morphism.
export Morphism.
theory Injections.
pred injective (f:'a -> 'b) =
forall (x y:'a), f x = f y => x = y.
pred cancel (f:'a -> 'b) (g:'b -> 'a) =
forall x, g (f x) = x.
pred pcancel (f:'a -> 'b) (g:'b -> 'a option) =
forall x, g (f x) = Some x.
pred ocancel (g:'b -> 'a option) h =
forall x, oapp h x (g x) = x.
lemma nosmt can_pcan (f:'a -> 'b) g: cancel f g => pcancel f (fun y, Some (g y)).
proof. by move=> fK x //=; congr; rewrite fK. qed.
lemma nosmt pcan_inj (f:'a -> 'b) g: pcancel f g => injective f.
proof.
move=> fK x y h; apply (congr1 g) in h.
by generalize h; rewrite !fK; apply someI.
qed.
lemma nosmt can_inj (f : 'a -> 'b) g: cancel f g => injective f.
proof. by move=> h; apply can_pcan in h; apply pcan_inj in h. 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.
end Injections.
export Injections.
theory InjectionsTheory.
lemma nosmt inj_id: injective (id<:'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 (comp f h).
proof. by move=> injf injh x y hy; apply injf in hy; apply injh. qed.
lemma nosmt can_comp (f:'b -> 'a) (h:'c -> 'b) f' h':
cancel f f' => cancel h h' => cancel (comp f h) (comp h' f').
proof. by move=> fK hK x; rewrite /comp /comp fK hK. qed.
lemma nosmt pcan_pcomp (f:'b -> 'a) (h:'c -> 'b) f' h':
pcancel f f' => pcancel h h' => pcancel (comp f h) (pcomp h' f').
proof. by move=> fK hK x; rewrite /comp /pcomp 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.
end InjectionsTheory.
export InjectionsTheory.
theory Bijections.
pred bijective (f:'b -> 'a) = exists g,
cancel f g /\ cancel g f.
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.
intros=> bijf; split=> fK; first by apply inj_can_sym; [apply fK | apply bij_inj].
by case bijf=> 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=> bijf.
rewrite -bij_can_sym // => fK.
rewrite -bij_can_sym // => fK'.
by apply (inj_can_eq f' f'' f)=> //; apply bij_inj.
qed.
end Bijections.
export Bijections.
theory BijectionsTheory.
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 (comp f h).
proof.
by move=> [f' [fK f'K]] [h' [hK h'K]]; exists (comp h' f'); split; apply can_comp.
qed.
lemma nosmt bij_can_bij (f:'b -> 'a): bijective f => forall f', cancel f f' => bijective f'.
proof.
case=> f' [fK f'K] g gK.
cut eqf'g:= bij_can_eq f f' g _ _ _=> //; first by exists f'.
by exists f; split; [apply (eq_can f' _ f) | apply (eq_can f _ f')].
qed.
end BijectionsTheory.
export BijectionsTheory.
theory Involutions.
pred involutive (f:'a -> 'a) = cancel f f.
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.
end Involutions.
export Involutions.
theory OperationProperties.
theory SopTisR.
pred left_inverse (e:'a) (inv:'a -> 'a) (o:'a -> 'a -> 'a) =
forall (x:'a), o (inv x) x = e.
pred right_inverse (e:'a) (inv:'a -> 'a) (o:'a -> 'a -> 'a) =
forall (x:'a), o x (inv x) = e.
pred left_injective (o:'a -> 'a -> 'a) =
forall (x y z:'a), o x y = o z y => x = z.
pred right_injective (o:'a -> 'a -> 'a) =
forall (x y z:'a), o x y = o x z => y = z.
end SopTisR.
export SopTisR.
theory SopTisS.
pred right_id e (o:'a -> 'b -> 'a) =
forall x, o x e = x.
pred left_zero z (o:'a -> 'b -> 'a) =
forall x, o z x = z.
pred right_commutative (o:'a -> 'b -> 'a) =
forall x y z, o (o x y) z = o (o x z) y.
pred left_distributive (o1:'a -> 'b -> 'a) (o2:'a -> 'a -> 'a) =
forall x y z, o1 (o2 x y) z = o2 (o1 x z) (o1 y z).
pred right_loop inv (o:'a -> 'b -> 'a) =
forall y, cancel (fun x, o x y) (fun x, o x (inv y)).
pred rev_right_loop inv (o:'a -> 'b -> 'a) =
forall y, cancel (fun x, o x (inv y)) (fun x, o x y).
end SopTisS.
export SopTisS.
theory SopTisT.
pred left_id e (o:'a -> 'b -> 'b) =
forall x, o e x = x.
pred right_zero z (o:'a -> 'b -> 'b) =
forall x, o x z = z.
pred left_commutative (o:'a -> 'b -> 'b) =
forall x y z, o x (o y z) = o y (o x z).
pred right_distributive (o:'a -> 'b -> 'b) add =
forall x y z, o x (add y z) = add (o x y) (o x z).
pred left_loop inv (o:'a -> 'b -> 'b) =
forall x, cancel (o x) (o (inv x)).
pred rev_left_loop inv (o:'a -> 'b -> 'b) =
forall x, cancel (o (inv x)) (o x).
end SopTisT.
export SopTisT.
theory SopSisT.
pred self_inverse e (o:'a -> 'a -> 'b) =
forall x, o x x = e.
pred commutative (o:'a -> 'a -> 'b) =
forall x y, o x y = o y x.
end SopSisT.
export SopSisT.
theory SopSisS.
pred idempotent (o:'a -> 'a -> 'a) =
forall x, o x x = x.
pred associative (o:'a -> 'a -> 'a) =
forall x y z, o x (o y z) = o (o x y) z.
pred interchange op1 op2 =
forall (x:'a) y z t, op1 (op2 x y) (op2 z t) = op2 (op1 x z) (op1 y t).
end SopSisS.
export SopSisS.
end OperationProperties.
export OperationProperties.
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.