swh:1:snp:deb9fd355bffe3d96f042bd4e5113afbb0d7cbb2
Tip revision: d5830863b50a5b59e77c7b3b888a1d3de33875d5 authored by Antoine Séré on 01 March 2021, 09:56:16 UTC
CRT prooved modulo some easy admits
CRT prooved modulo some easy admits
Tip revision: d583086
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.