Skip to content
Snippets Groups Projects
Commit 6f31e0eb authored by Simon Spies's avatar Simon Spies
Browse files

add iris prelude

parent 7c06b30a
No related branches found
No related tags found
No related merge requests found
(** * extensional model using ϵ, PE and FE *)
From iris.prelude Require Export prelude.
Require Import Coq.Logic.Epsilon.
Require Import Coq.Logic.PropExtensionality.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Logic.Classical_Prop.
(* some classical reasoning principles *)
Lemma classic_or_to_sum (P Q : Prop) : P Q P + Q.
Proof.
intros HPQ. assert (exists (b : bool), if b then P else Q) as Hex.
{ destruct HPQ; by [exists true|exists false]. }
apply constructive_indefinite_description in Hex as [[] ?]; eauto.
Qed.
Lemma classic_dn (X : Prop) : ¬ (¬ X) X.
Proof.
destruct (classic X); tauto.
Qed.
Lemma classic_forall_exists_dn (X : Type) (P : X Prop): ( x, P x) ¬ ( x, ¬ (P x)).
Proof.
split.
- intros H (x & H1). eauto.
- intros H x. destruct (classic (P x)) as [| ?]; first done.
exfalso; apply H; eauto.
Qed.
Lemma classic_not_forall X (P: X Prop): ¬ ( x: X, P x) x: X, ¬ P x.
Proof.
by rewrite classic_forall_exists_dn classic_dn.
Qed.
Lemma classic_not_exists X (P: X Prop): ¬ ( x: X, P x) x: X, ¬ P x.
Proof.
by rewrite classic_forall_exists_dn; split; intros H [x ?]; eauto using classic_dn.
Qed.
Lemma classic_not_impl (P Q: Prop): ¬ (P Q) P ¬ Q.
Proof.
destruct (classic P); tauto.
Qed.
Lemma classic_find_least {X: Type} (R: X X Prop) (P: X Prop) x:
wf R
( x y, R x y P x P y)
P x
y, P y x, R x y ¬ P x.
Proof.
intros Hwf HP. induction (Hwf x) as [x _ IH].
intros Hx. destruct (classic ( y, R y x ¬ P y)) as [|Hn]; first by eauto.
revert Hn; rewrite classic_not_forall=> [[y]]; rewrite classic_not_impl classic_dn.
intros []; eauto.
Qed.
(* we use classical logic to define a normalizer function
for building quotients *)
Section quotients.
Context {X: Type} (R: X X Prop) `{Equivalence X R}.
Definition norm (x: X) := epsilon (inhabits x) (R x).
Lemma rel_norm x y: R x y norm x = norm y.
Proof.
intros HR; unfold norm; f_equal.
- apply proof_irrelevance.
- eapply functional_extensionality; intros u; eapply propositional_extensionality.
by rewrite HR.
Qed.
Lemma norm_pi s (Hq Hq': norm s = s): Hq = Hq'.
Proof.
apply proof_irrelevance.
Qed.
Lemma rel_norm_intro x: R x (norm x).
Proof.
unfold norm; eapply epsilon_spec; exists x; reflexivity.
Qed.
(* derived lemmas *)
Lemma norm_idem x: norm (norm x) = norm x.
Proof.
eapply rel_norm; symmetry; eapply rel_norm_intro.
Qed.
Lemma norm_rel x y: norm x = norm y R x y.
Proof.
by intros Heq; rewrite (rel_norm_intro x) (rel_norm_intro y) Heq.
Qed.
Lemma norm_iff x y: norm x = norm y R x y.
Proof.
split; eauto using rel_norm, norm_rel.
Qed.
Global Instance norm_proper : Proper (R ==> R) norm.
Proof.
intros x y HR. by rewrite -(rel_norm_intro x) -(rel_norm_intro y).
Qed.
End quotients.
\ No newline at end of file
(** Coq configuration for Iris (not meant to leak to clients) *)
(* Everything here should be [Export Set], which means when this
file is *imported*, the option will only apply on the import site
but not transitively. *)
Export Set Default Proof Using "Type".
Export Set Suggest Proof Using. (* also warns about forgotten [Proof.] *)
(* Enforces that every tactic is executed with a single focused goal, meaning
that bullets and curly braces must be used to structure the proof. *)
Export Set Default Goal Selector "!".
(* We always annotate hints with locality ([Global] or [Local]). This enforces
that at least global hints are annotated. *)
Export Set Warnings "+deprecated-hint-without-locality".
(* "Fake" import to whitelist this file for the check that ensures we import
this file everywhere.
From iris.prelude Require Import options.
*)
From Coq.ssr Require Export ssreflect.
From stdpp Require Export prelude.
From iris.prelude Require Import options.
Global Open Scope general_if_scope.
Global Set SsrOldRewriteGoalsOrder. (* See Coq issue #5706 *)
Ltac done := stdpp.tactics.done.
(** Iris itself and many dependencies still rely on this coercion. *)
Coercion Z.of_nat : nat >-> Z.
(* some basic definitions and lemmas *)
Inductive rc {A} (R: A A Prop) (x: A) (y: A): Prop :=
| rc_refl: x = y rc R x y
| rc_subrel: R x y rc R x y.
Global Hint Constructors rc : core.
Global Instance rc_reflexive {A} (R : A A Prop) : Reflexive (rc R).
Proof. intros ?; by apply rc_refl. Qed.
Global Instance rc_subrelation {A} (R : A A Prop): subrelation R (rc R).
Proof. intros ? ? ?; by apply rc_subrel. Qed.
Lemma rc_iff {A} (R: A A Prop) x y: rc R x y R x y x = y.
Proof.
split; destruct 1; eauto.
Qed.
Global Instance rc_transitive {A} (R: A A Prop) `{!Transitive R}: Transitive (rc R).
Proof.
intros x y z [] []; subst; eauto.
Qed.
(* this is not classical, but useful *)
Lemma ex_impl X (P: X Prop) (Q: Prop): (( x, P x) Q) x, P x Q.
Proof.
split.
- intros H x Px; eapply H; by exists x.
- intros HPQ [x Px]; eauto.
Qed.
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment