swh:1:snp:04e159a4411e97cbe416dcf21d082639f654120b
Tip revision: b40d073921a3c81ad7091006d32daeb51725fc76 authored by Adrien Koutsos on 28 June 2021, 12:17:13 UTC
fixed PKE
fixed PKE
Tip revision: b40d073
Quotient.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
* -------------------------------------------------------------------- *)
require Subtype.
pragma +implicits.
(* -------------------------------------------------------------------- *)
(* This theory defines the effective quotient [qT] obtained from [T] *)
(* via a representative/canonical surjecton pair of functions. *)
(* -------------------------------------------------------------------- *)
abstract theory CoreQuotient.
type T, qT.
op repr : qT -> T. (* representative selection *)
op pi : T -> qT. (* canonical surjection *)
axiom reprK: cancel repr pi.
op (==) (x y : T) = (pi x = pi y).
(* -------------------------------------------------------------------- *)
lemma piP (x : T): x == repr (pi x).
proof. by rewrite /(==) reprK. qed.
lemma quotW P: (forall y, P (pi y)) => forall x, P x.
proof. by move=> Py x; rewrite -(reprK x); apply/Py. qed.
lemma quotP P: (forall y, repr (pi y) = y => P (pi y)) => forall x, P x.
proof. by move=> Py x; rewrite -(reprK x); apply/Py; rewrite reprK. qed.
end CoreQuotient.
(* -------------------------------------------------------------------- *)
(* This theory defines the effective quotient by an equivalence *)
(* relation. It is build on the former theory, using for [qT] the *)
(* elements of [T] that are stable by repr \o pi. *)
(* -------------------------------------------------------------------- *)
abstract theory EquivQuotient.
type T.
op eqv : T -> T -> bool.
theory EqvEquiv.
axiom eqv_refl : reflexive eqv.
axiom eqv_sym : symmetric eqv.
axiom eqv_trans: transitive eqv.
end EqvEquiv.
import EqvEquiv.
lemma eqv_choose (x : T): exists y, eqv x y.
proof. by exists x; rewrite eqv_refl. qed.
op canon (x : T) = choiceb (eqv x) x.
lemma eqv_canon (x : T) : eqv x (canon x).
proof.
rewrite /canon; apply: (@choicebP (eqv x) x).
by exists x; apply: eqv_refl.
qed.
lemma eqv_canon_eq (x y : T): eqv x y => canon x = canon y.
proof.
move=> eqv_xy; rewrite /canon (@eq_choice (eqv x) (eqv y)).
- move=> z; split => [eqv_xz|eqv_yz].
- by apply/(eqv_trans x) => //; rewrite eqv_sym.
- by apply/(eqv_trans _ eqv_xy eqv_yz).
by apply: choice_dfl_irrelevant; exists y; apply: eqv_refl.
qed.
lemma canonK x : canon (canon x) = canon x.
proof. by rewrite &(eqv_canon_eq) eqv_sym eqv_canon. qed.
op iscanon x = canon x = x.
lemma canon_iscanon x : iscanon x => canon x = x.
proof. by move=> @/iscanon /eq_sym ->; apply: canonK. qed.
lemma iscanon_canon x : iscanon (canon x).
proof. by rewrite /iscanon canonK. qed.
lemma eqvP x y : (eqv x y) <=> (canon x = canon y).
proof.
split=> [/eqv_canon_eq //|eq].
rewrite &(eqv_trans (canon y)) -1:eqv_sym -1:eqv_canon.
apply/(eqv_trans (canon x)); first by apply/eqv_canon.
by rewrite eq &(eqv_refl).
qed.
type qT.
clone import Subtype with
type T <- T,
type sT <- qT,
pred P <- iscanon,
op wsT <- canon witness.
clone include CoreQuotient with
type T <- T,
type qT <- qT,
op pi = fun x => Subtype.insubd (canon x),
op repr = fun x => Subtype.val x
proof *.
realize reprK. proof.
by move=> q; rewrite /pi /repr /insubd canon_iscanon 1:valP valK.
qed.
lemma eqv_pi : forall x y , eqv x y <=> pi x = pi y.
proof.
move=> x y @/pi; split=> [eq_xy|]; first by congr; apply: eqv_canon_eq.
by move/(congr1 val); rewrite !val_insubd !iscanon_canon /= => /eqvP.
qed.
lemma eqv_repr : forall x, eqv (repr (pi x)) x.
proof.
move=> x @/pi @/repr; rewrite val_insubd.
by rewrite iscanon_canon /= eqv_sym &(eqv_canon).
qed.
end EquivQuotient.