Commit 599d7411 authored by Ralf Jung's avatar Ralf Jung

improve coq 8.6 compatibility

parent 8f33e282
Pipeline #3001 passed with stage
in 10 minutes
......@@ -34,7 +34,6 @@ prelude/lexico.v
prelude/set.v
prelude/decidable.v
prelude/list.v
prelude/error.v
prelude/functions.v
prelude/hlist.v
prelude/sorting.v
......
......@@ -837,7 +837,8 @@ Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch.
collection of type [C] that contains the keys that are a member of [m]. *)
Class Dom (M C : Type) := dom: M C.
Instance: Params (@dom) 3.
Arguments dom {_} _ {_} !_ / : simpl nomatch, clear implicits.
Arguments dom _ _ _ _ : clear implicits.
Arguments dom {_} _ {_} !_ / : simpl nomatch.
(** The function [merge f m1 m2] should merge the maps [m1] and [m2] by
constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)].*)
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
From iris.prelude Require Export list.
Definition error (S E A : Type) : Type := S E + (A * S).
Definition error_eval {S E A} (x : error S E A) (s : S) : E + A :=
match x s with inl e => inl e | inr (a,_) => inr a end.
Instance error_ret {S E} : MRet (error S E) := λ A x s, inr (x,s).
Instance error_bind {S E} : MBind (error S E) := λ A B f x s,
match x s with
| inr (a,s') => f a s'
| inl e => inl e
end.
Instance error_fmap {S E} : FMap (error S E) := λ A B f x s,
match x s with
| inr (a,s') => inr (f a,s')
| inl e => inl e
end.
Definition fail {S E A} (e : E) : error S E A := λ s, inl e.
Definition modify {S E} (f : S S) : error S E () := λ s, inr ((), f s).
Definition gets {S E A} (f : S A) : error S E A := λ s, inr (f s, s).
Definition error_guard {E} P {dec : Decision P} {S A}
(e : E) (f : P error S E A) : error S E A :=
match decide P with left H => f H | right _ => fail e end.
Notation "'guard' P 'with' e ; o" := (error_guard P e (λ _, o))
(at level 65, only parsing, right associativity) : C_scope.
Definition error_of_option {S A E} (x : option A) (e : E) : error S E A :=
match x with Some a => mret a | None => fail e end.
Lemma error_bind_ret {S E A B} (f : A error S E B) s s'' x b :
(x = f) s = mret b s'' a s', x s = mret a s' f a s' = mret b s''.
Proof. compute; destruct (x s) as [|[??]]; naive_solver. Qed.
Lemma error_fmap_ret {S E A B} (f : A B) s s' (x : error S E A) b :
(f <$> x) s = mret b s' a, x s = mret a s' b = f a.
Proof. compute; destruct (x s) as [|[??]]; naive_solver. Qed.
Lemma error_of_option_ret {S E A} (s s' : S) (o : option A) (e : E) a :
error_of_option o e s = mret a s' o = Some a s = s'.
Proof. compute; destruct o; naive_solver. Qed.
Lemma error_guard_ret {S E A} `{dec : Decision P} s s' (x : error S E A) e a :
(guard P with e ; x) s = mret a s' P x s = mret a s'.
Proof. compute; destruct dec; naive_solver. Qed.
Lemma error_fmap_bind {S E A B C} (f : A B) (g : B error S E C) x s :
((f <$> x) = g) s = (x = g f) s.
Proof. by compute; destruct (x s) as [|[??]]. Qed.
Lemma error_assoc {S E A B C} (f : A error S E B) (g : B error S E C) x s :
((x = f) = g) s = (a x; f a = g) s.
Proof. by compute; destruct (x s) as [|[??]]. Qed.
Lemma error_of_option_bind {S E A B} (f : A option B) o e :
error_of_option (S := S) (E:=E) (o = f) e
= a error_of_option o e; error_of_option (f a) e.
Proof. by destruct o. Qed.
Lemma error_gets_spec {S E A} (g : S A) s : gets (E:=E) g s = mret (g s) s.
Proof. done. Qed.
Lemma error_modify_spec {S E} (g : S S) s : modify (E:=E) g s = mret () (g s).
Proof. done. Qed.
Lemma error_left_gets {S E A B} (g : S A) (f : A error S E B) s :
(gets (E:=E) g = f) s = f (g s) s.
Proof. done. Qed.
Lemma error_left_modify {S E B} (g : S S) (f : unit error S E B) s :
(modify (E:=E) g = f) s = f () (g s).
Proof. done. Qed.
Lemma error_left_id {S E A B} (a : A) (f : A error S E B) :
(mret a = f) = f a.
Proof. done. Qed.
Ltac generalize_errors :=
csimpl;
let gen_error e :=
try (is_var e; fail 1); generalize e;
let x := fresh "err" in intros x in
repeat match goal with
| |- appcontext[ fail ?e ] => gen_error e
| |- appcontext[ error_guard _ ?e ] => gen_error e
| |- appcontext[ error_of_option _ ?e ] => gen_error e
end.
Tactic Notation "simplify_error_equality" :=
repeat match goal with
| H : context [ gets _ _ _ ] |- _ => rewrite error_gets_spec in H
| H : context [ modify _ _ _ ] |- _ => rewrite error_modify_spec in H
| H : (mret (M:=error _ _) _ = _) _ = _ |- _ => rewrite error_left_id in H
| H : (gets _ = _) _ = _ |- _ => rewrite error_left_gets in H
| H : (modify _ = _) _ = _ |- _ => rewrite error_left_modify in H
| H : error_guard _ _ _ _ = _ |- _ => apply error_guard_ret in H; destruct H
| _ => progress simplify_eq/=
| H : error_of_option _ _ _ = _ |- _ =>
apply error_of_option_ret in H; destruct H
| H : mbind (M:=error _ _) _ _ _ = _ |- _ =>
apply error_bind_ret in H; destruct H as (?&?&?&?)
| H : fmap (M:=error _ _) _ _ _ = _ |- _ =>
apply error_fmap_ret in H; destruct H as (?&?&?)
| H : mbind (M:=option) _ _ = _ |- _ =>
apply bind_Some in H; destruct H as (?&?&?)
| H : fmap (M:=option) _ _ = _ |- _ =>
apply fmap_Some in H; destruct H as (?&?&?)
| H : maybe _ ?x = Some _ |- _ => is_var x; destruct x
| H : maybe2 _ ?x = Some _ |- _ => is_var x; destruct x
| H : maybe3 _ ?x = Some _ |- _ => is_var x; destruct x
| H : maybe4 _ ?x = Some _ |- _ => is_var x; destruct x
| _ => progress case_decide
end.
Tactic Notation "error_proceed" :=
repeat match goal with
| H : context [ gets _ _ ] |- _ => rewrite error_gets_spec in H
| H : context [ modify _ _ ] |- _ => rewrite error_modify_spec in H
| H : context [ error_of_option _ _ ] |- _ => rewrite error_of_option_bind in H
| H : (mret (M:= _ _) _ = _) _ = _ |- _ => rewrite error_left_id in H
| H : (gets _ = _) _ = _ |- _ => rewrite error_left_gets in H
| H : (modify _ = _) _ = _ |- _ => rewrite error_left_modify in H
| H : ((_ <$> _) = _) _ = _ |- _ => rewrite error_fmap_bind in H
| H : ((_ = _) = _) _ = _ |- _ => rewrite error_assoc in H
| H : (error_guard _ _ _) _ = _ |- _ =>
let H' := fresh in apply error_guard_ret in H; destruct H as [H' H]
| _ => progress simplify_eq/=
| H : maybe _ ?x = Some _ |- _ => is_var x; destruct x
| H : maybe2 _ ?x = Some _ |- _ => is_var x; destruct x
| H : maybe3 _ ?x = Some _ |- _ => is_var x; destruct x
| H : maybe4 _ ?x = Some _ |- _ => is_var x; destruct x
end.
Tactic Notation "error_proceed"
simple_intropattern(a) "as" simple_intropattern(s) :=
error_proceed;
lazymatch goal with
| H : (error_of_option ?o _ = _) _ = _ |- _ => destruct o as [a|] eqn:?
| H : error_of_option ?o _ _ = _ |- _ => destruct o as [a|] eqn:?
| H : (_ = _) _ = _ |- _ => apply error_bind_ret in H; destruct H as (a&s&?&H)
| H : (_ <$> _) _ = _ |- _ => apply error_fmap_ret in H; destruct H as (a&?&?)
end;
error_proceed.
......@@ -7,8 +7,10 @@ Class Finite A `{EqDecision A} := {
NoDup_enum : NoDup enum;
elem_of_enum x : x enum
}.
Arguments enum _ {_ _} : clear implicits.
Arguments NoDup_enum _ {_ _} : clear implicits.
Arguments enum _ _ _ : clear implicits.
Arguments enum _ {_ _}.
Arguments NoDup_enum _ _ _ : clear implicits.
Arguments NoDup_enum _ {_ _}.
Definition card A `{Finite A} := length (enum A).
Program Instance finite_countable `{Finite A} : Countable A := {|
encode := λ x,
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment