swh:1:snp:04e159a4411e97cbe416dcf21d082639f654120b
Tip revision: 846710a2a656834065e745d19416ebdc83158f55 authored by Benjamin Gregoire on 14 July 2019, 06:50:07 UTC
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Tip revision: 846710a
Subtype.eca
(* --------------------------------------------------------------------
* 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
* -------------------------------------------------------------------- *)
pragma +implicits.
(* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
(* This theory defines the subtype [sT] of [T] defined as {x : T | P x} *)
(* where P is a predicate over T. This subtype is defined via an *)
(* axiomatization of an inversible partial projection from [T] to [sT] *)
(* that respects [P]. *)
(* *)
(* Injection from [sT] to [T] and (partial) projection of [T] to [sT] *)
(* val == generic injection from [sT] to [T] *)
(* insub == generic partial projection from [T] to [sT] *)
(* *)
(* {x : T | P x} and [sT] are in bijection via val/insub. *)
(* 1. insub x = None if !(P x) *)
(* 2. insub x = Some y with val y = x if (P x) *)
(* -------------------------------------------------------------------- *)
require import Core.
type T, sT.
pred P : T.
op insub : T -> sT option.
op val : sT -> T.
axiom insubN (x : T): !P x => insub x = None.
axiom insubT (x : T): P x => omap val (insub x) = Some x.
axiom valP (x : sT): P (val x).
axiom valK: pcancel val insub.
(* -------------------------------------------------------------------- *)
(* EasyCrypt types cannot be empty. We here explicitely provide the *)
(* inverse element of default inhabitant of [sT] *)
op wsT : T.
axiom insubW: insub wsT = Some witness<:sT>.
(* -------------------------------------------------------------------- *)
op insubd (x : T) = odflt witness (insub x).
(* -------------------------------------------------------------------- *)
lemma val_inj: injective val.
proof. by apply/(pcan_inj _ _ valK). qed.
lemma valKd: cancel val insubd.
proof. by move=> u; rewrite /insubd valK. qed.
lemma insubP (x : T): (* We need inductive predicates *)
(exists u, P x /\ insub x = Some u /\ val u = x)
\/ (!P x /\ insub x = None).
proof. (* this proof script is awful *)
case (P x)=> [Px | /insubN -> //]; left.
move: Px => /insubT; case {-2}(insub x) (eq_refl (insub x))=> //.
by move=> /= u eq_insub eqx; exists u => /=; move: eqx => ->.
qed.
lemma val_insubd x: val (insubd x) = if P x then x else val witness.
proof. by rewrite /insubd; case (insubP x) => [[u] [->] [->]|[-> ->]]. qed.
lemma insubdK (x : T): P x => val (insubd x) = x.
proof. by move=> Px; rewrite val_insubd Px. qed.
(* -------------------------------------------------------------------- *)
theory Lift.
op lift1 (f : T -> T) =
fun (z : sT), insubd (f (val z)).
op lift2 (f : T -> T -> T) =
fun (z1 z2 : sT), insubd (f (val z1) (val z2)).
lemma lift1E (f : T -> T):
(forall x, P x => P (f x))
=> forall x, val (lift1 f x) = f (val x).
proof. by move=> h x; rewrite /lift1 insubdK ?h ?valP. qed.
lemma lift2E (f : T -> T -> T):
(forall x y, P x => P y => P (f x y))
=> forall x y, val (lift2 f x y) = f (val x) (val y).
proof. by move=> h x y; rewrite /lift2 insubdK ?h ?valP. qed.
end Lift.