Commit 24aef2fe authored by Robbert Krebbers's avatar Robbert Krebbers

Make uses of Arguments more rubust.

See also Coq bug #5712.
parent dc7a3a89
Pipeline #4377 passed with stage
in 6 minutes and 33 seconds
This diff is collapsed.
...@@ -5,8 +5,9 @@ From stdpp Require Export prelude. ...@@ -5,8 +5,9 @@ From stdpp Require Export prelude.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Record bset (A : Type) : Type := mkBSet { bset_car : A bool }. Record bset (A : Type) : Type := mkBSet { bset_car : A bool }.
Arguments mkBSet {_} _. Arguments mkBSet {_} _ : assert.
Arguments bset_car {_} _ _. Arguments bset_car {_} _ _ : assert.
Instance bset_top {A} : Top (bset A) := mkBSet (λ _, true). Instance bset_top {A} : Top (bset A) := mkBSet (λ _, true).
Instance bset_empty {A} : Empty (bset A) := mkBSet (λ _, false). Instance bset_empty {A} : Empty (bset A) := mkBSet (λ _, false).
Instance bset_singleton `{EqDecision A} : Singleton A (bset A) := λ x, Instance bset_singleton `{EqDecision A} : Singleton A (bset A) := λ x,
......
...@@ -30,7 +30,7 @@ Fixpoint coPset_wf (t : coPset_raw) : bool := ...@@ -30,7 +30,7 @@ Fixpoint coPset_wf (t : coPset_raw) : bool :=
| coPNode false (coPLeaf false) (coPLeaf false) => false | coPNode false (coPLeaf false) (coPLeaf false) => false
| coPNode b l r => coPset_wf l && coPset_wf r | coPNode b l r => coPset_wf l && coPset_wf r
end. end.
Arguments coPset_wf !_ / : simpl nomatch. Arguments coPset_wf !_ / : simpl nomatch, assert.
Lemma coPNode_wf_l b l r : coPset_wf (coPNode b l r) coPset_wf l. Lemma coPNode_wf_l b l r : coPset_wf (coPNode b l r) coPset_wf l.
Proof. destruct b, l as [[]|],r as [[]|]; simpl; rewrite ?andb_True; tauto. Qed. Proof. destruct b, l as [[]|],r as [[]|]; simpl; rewrite ?andb_True; tauto. Qed.
...@@ -44,7 +44,7 @@ Definition coPNode' (b : bool) (l r : coPset_raw) : coPset_raw := ...@@ -44,7 +44,7 @@ Definition coPNode' (b : bool) (l r : coPset_raw) : coPset_raw :=
| false, coPLeaf false, coPLeaf false => coPLeaf false | false, coPLeaf false, coPLeaf false => coPLeaf false
| _, _, _ => coPNode b l r | _, _, _ => coPNode b l r
end. end.
Arguments coPNode' _ _ _ : simpl never. Arguments coPNode' : simpl never.
Lemma coPNode_wf b l r : coPset_wf l coPset_wf r coPset_wf (coPNode' b l r). Lemma coPNode_wf b l r : coPset_wf l coPset_wf r coPset_wf (coPNode' b l r).
Proof. destruct b, l as [[]|], r as [[]|]; simpl; auto. Qed. Proof. destruct b, l as [[]|], r as [[]|]; simpl; auto. Qed.
Hint Resolve coPNode_wf. Hint Resolve coPNode_wf.
...@@ -57,7 +57,7 @@ Fixpoint coPset_elem_of_raw (p : positive) (t : coPset_raw) {struct t} : bool := ...@@ -57,7 +57,7 @@ Fixpoint coPset_elem_of_raw (p : positive) (t : coPset_raw) {struct t} : bool :=
| coPNode _ _ r, p~1 => coPset_elem_of_raw p r | coPNode _ _ r, p~1 => coPset_elem_of_raw p r
end. end.
Local Notation e_of := coPset_elem_of_raw. Local Notation e_of := coPset_elem_of_raw.
Arguments coPset_elem_of_raw _ !_ / : simpl nomatch. Arguments coPset_elem_of_raw _ !_ / : simpl nomatch, assert.
Lemma coPset_elem_of_node b l r p : Lemma coPset_elem_of_node b l r p :
e_of p (coPNode' b l r) = e_of p (coPNode b l r). e_of p (coPNode' b l r) = e_of p (coPNode b l r).
Proof. by destruct p, b, l as [[]|], r as [[]|]. Qed. Proof. by destruct p, b, l as [[]|], r as [[]|]. Qed.
...@@ -99,7 +99,7 @@ Instance coPset_union_raw : Union coPset_raw := ...@@ -99,7 +99,7 @@ Instance coPset_union_raw : Union coPset_raw :=
| coPLeaf false, coPNode b l r => coPNode b l r | coPLeaf false, coPNode b l r => coPNode b l r
| coPNode b1 l1 r1, coPNode b2 l2 r2 => coPNode' (b1||b2) (l1 l2) (r1 r2) | coPNode b1 l1 r1, coPNode b2 l2 r2 => coPNode' (b1||b2) (l1 l2) (r1 r2)
end. end.
Local Arguments union _ _!_ !_ /. Local Arguments union _ _!_ !_ / : assert.
Instance coPset_intersection_raw : Intersection coPset_raw := Instance coPset_intersection_raw : Intersection coPset_raw :=
fix go t1 t2 := let _ : Intersection _ := @go in fix go t1 t2 := let _ : Intersection _ := @go in
match t1, t2 with match t1, t2 with
...@@ -110,7 +110,7 @@ Instance coPset_intersection_raw : Intersection coPset_raw := ...@@ -110,7 +110,7 @@ Instance coPset_intersection_raw : Intersection coPset_raw :=
| coPLeaf true, coPNode b l r => coPNode b l r | coPLeaf true, coPNode b l r => coPNode b l r
| coPNode b1 l1 r1, coPNode b2 l2 r2 => coPNode' (b1&&b2) (l1 l2) (r1 r2) | coPNode b1 l1 r1, coPNode b2 l2 r2 => coPNode' (b1&&b2) (l1 l2) (r1 r2)
end. end.
Local Arguments intersection _ _!_ !_ /. Local Arguments intersection _ _!_ !_ / : assert.
Fixpoint coPset_opp_raw (t : coPset_raw) : coPset_raw := Fixpoint coPset_opp_raw (t : coPset_raw) : coPset_raw :=
match t with match t with
| coPLeaf b => coPLeaf (negb b) | coPLeaf b => coPLeaf (negb b)
......
...@@ -92,7 +92,7 @@ This transformation is implemented using type classes instead of setoid ...@@ -92,7 +92,7 @@ This transformation is implemented using type classes instead of setoid
rewriting to ensure that we traverse each term at most once and to be able to rewriting to ensure that we traverse each term at most once and to be able to
deal with occurences of the set operations under binders. *) deal with occurences of the set operations under binders. *)
Class SetUnfold (P Q : Prop) := { set_unfold : P Q }. Class SetUnfold (P Q : Prop) := { set_unfold : P Q }.
Arguments set_unfold _ _ {_}. Arguments set_unfold _ _ {_} : assert.
Hint Mode SetUnfold + - : typeclass_instances. Hint Mode SetUnfold + - : typeclass_instances.
Class SetUnfoldSimpl (P Q : Prop) := { set_unfold_simpl : SetUnfold P Q }. Class SetUnfoldSimpl (P Q : Prop) := { set_unfold_simpl : SetUnfold P Q }.
......
...@@ -18,7 +18,7 @@ Notation fin := Fin.t. ...@@ -18,7 +18,7 @@ Notation fin := Fin.t.
Notation FS := Fin.FS. Notation FS := Fin.FS.
Delimit Scope fin_scope with fin. Delimit Scope fin_scope with fin.
Arguments Fin.FS _ _%fin. Arguments Fin.FS _ _%fin : assert.
Notation "0" := Fin.F1 : fin_scope. Notation "1" := (FS 0) : fin_scope. Notation "0" := Fin.F1 : fin_scope. Notation "1" := (FS 0) : fin_scope.
Notation "2" := (FS 1) : fin_scope. Notation "3" := (FS 2) : fin_scope. Notation "2" := (FS 1) : fin_scope. Notation "3" := (FS 2) : fin_scope.
......
...@@ -8,17 +8,17 @@ Class Finite A `{EqDecision A} := { ...@@ -8,17 +8,17 @@ Class Finite A `{EqDecision A} := {
NoDup_enum : NoDup enum; NoDup_enum : NoDup enum;
elem_of_enum x : x enum elem_of_enum x : x enum
}. }.
Arguments enum _ _ _ : clear implicits. Arguments enum : clear implicits.
Arguments enum _ {_ _}. Arguments enum _ {_ _} : assert.
Arguments NoDup_enum _ _ _ : clear implicits. Arguments NoDup_enum : clear implicits.
Arguments NoDup_enum _ {_ _}. Arguments NoDup_enum _ {_ _} : assert.
Definition card A `{Finite A} := length (enum A). Definition card A `{Finite A} := length (enum A).
Program Instance finite_countable `{Finite A} : Countable A := {| Program Instance finite_countable `{Finite A} : Countable A := {|
encode := λ x, encode := λ x,
Pos.of_nat $ S $ from_option id 0 $ fst <$> list_find (x =) (enum A); Pos.of_nat $ S $ from_option id 0 $ fst <$> list_find (x =) (enum A);
decode := λ p, enum A !! pred (Pos.to_nat p) decode := λ p, enum A !! pred (Pos.to_nat p)
|}. |}.
Arguments Pos.of_nat _ : simpl never. Arguments Pos.of_nat : simpl never.
Next Obligation. Next Obligation.
intros ?? [xs Hxs HA] x; unfold encode, decode; simpl. intros ?? [xs Hxs HA] x; unfold encode, decode; simpl.
destruct (list_find_elem_of (x =) xs x) as [[i y] Hi]; auto. destruct (list_find_elem_of (x =) xs x) as [[i y] Hi]; auto.
......
...@@ -15,8 +15,8 @@ Record gmap K `{Countable K} A := GMap { ...@@ -15,8 +15,8 @@ Record gmap K `{Countable K} A := GMap {
gmap_car : Pmap A; gmap_car : Pmap A;
gmap_prf : bool_decide (gmap_wf gmap_car) gmap_prf : bool_decide (gmap_wf gmap_car)
}. }.
Arguments GMap {_ _ _ _} _ _. Arguments GMap {_ _ _ _} _ _ : assert.
Arguments gmap_car {_ _ _ _} _. Arguments gmap_car {_ _ _ _} _ : assert.
Lemma gmap_eq `{Countable K} {A} (m1 m2 : gmap K A) : Lemma gmap_eq `{Countable K} {A} (m1 m2 : gmap K A) :
m1 = m2 gmap_car m1 = gmap_car m2. m1 = m2 gmap_car m1 = gmap_car m2.
Proof. Proof.
......
...@@ -4,8 +4,8 @@ From stdpp Require Import gmap. ...@@ -4,8 +4,8 @@ From stdpp Require Import gmap.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Record gmultiset A `{Countable A} := GMultiSet { gmultiset_car : gmap A nat }. Record gmultiset A `{Countable A} := GMultiSet { gmultiset_car : gmap A nat }.
Arguments GMultiSet {_ _ _} _. Arguments GMultiSet {_ _ _} _ : assert.
Arguments gmultiset_car {_ _ _} _. Arguments gmultiset_car {_ _ _} _ : assert.
Lemma gmultiset_eq_dec `{Countable A} : EqDecision (gmultiset A). Lemma gmultiset_eq_dec `{Countable A} : EqDecision (gmultiset A).
Proof. solve_decision. Defined. Proof. solve_decision. Defined.
......
...@@ -12,8 +12,8 @@ Record hashset {A} (hash : A → Z) := Hashset { ...@@ -12,8 +12,8 @@ Record hashset {A} (hash : A → Z) := Hashset {
hashset_prf : hashset_prf :
map_Forall (λ n l, Forall (λ x, hash x = n) l NoDup l) hashset_car map_Forall (λ n l, Forall (λ x, hash x = n) l NoDup l) hashset_car
}. }.
Arguments Hashset {_ _} _ _. Arguments Hashset {_ _} _ _ : assert.
Arguments hashset_car {_ _} _. Arguments hashset_car {_ _} _ : assert.
Section hashset. Section hashset.
Context `{EqDecision A} (hash : A Z). Context `{EqDecision A} (hash : A Z).
......
...@@ -37,7 +37,7 @@ Fixpoint himpl (As : tlist) (B : Type) : Type := ...@@ -37,7 +37,7 @@ Fixpoint himpl (As : tlist) (B : Type) : Type :=
Definition hinit {B} (y : B) : himpl tnil B := y. Definition hinit {B} (y : B) : himpl tnil B := y.
Definition hlam {A As B} (f : A himpl As B) : himpl (tcons A As) B := f. Definition hlam {A As B} (f : A himpl As B) : himpl (tcons A As) B := f.
Arguments hlam _ _ _ _ _/. Arguments hlam _ _ _ _ _ / : assert.
Definition hcurry {As B} (f : himpl As B) (xs : hlist As) : B := Definition hcurry {As B} (f : himpl As B) (xs : hlist As) : B :=
(fix go As xs := (fix go As xs :=
......
...@@ -6,9 +6,9 @@ From Coq Require Export Permutation. ...@@ -6,9 +6,9 @@ From Coq Require Export Permutation.
From stdpp Require Export numbers base option. From stdpp Require Export numbers base option.
Set Default Proof Using "Type*". Set Default Proof Using "Type*".
Arguments length {_} _. Arguments length {_} _ : assert.
Arguments cons {_} _ _. Arguments cons {_} _ _ : assert.
Arguments app {_} _ _. Arguments app {_} _ _ : assert.
Instance: Params (@length) 1. Instance: Params (@length) 1.
Instance: Params (@cons) 1. Instance: Params (@cons) 1.
...@@ -18,16 +18,16 @@ Notation tail := tl. ...@@ -18,16 +18,16 @@ Notation tail := tl.
Notation take := firstn. Notation take := firstn.
Notation drop := skipn. Notation drop := skipn.
Arguments tail {_} _. Arguments tail {_} _ : assert.
Arguments take {_} !_ !_ /. Arguments take {_} !_ !_ / : assert.
Arguments drop {_} !_ !_ /. Arguments drop {_} !_ !_ / : assert.
Instance: Params (@tail) 1. Instance: Params (@tail) 1.
Instance: Params (@take) 1. Instance: Params (@take) 1.
Instance: Params (@drop) 1. Instance: Params (@drop) 1.
Arguments Permutation {_} _ _. Arguments Permutation {_} _ _ : assert.
Arguments Forall_cons {_} _ _ _ _ _. Arguments Forall_cons {_} _ _ _ _ _ : assert.
Remove Hints Permutation_cons : typeclass_instances. Remove Hints Permutation_cons : typeclass_instances.
Notation "(::)" := cons (only parsing) : C_scope. Notation "(::)" := cons (only parsing) : C_scope.
...@@ -148,7 +148,7 @@ Fixpoint resize {A} (n : nat) (y : A) (l : list A) : list A := ...@@ -148,7 +148,7 @@ Fixpoint resize {A} (n : nat) (y : A) (l : list A) : list A :=
| [] => replicate n y | [] => replicate n y
| x :: l => match n with 0 => [] | S n => x :: resize n y l end | x :: l => match n with 0 => [] | S n => x :: resize n y l end
end. end.
Arguments resize {_} !_ _ !_. Arguments resize {_} !_ _ !_ : assert.
Instance: Params (@resize) 2. Instance: Params (@resize) 2.
(** The function [reshape k l] transforms [l] into a list of lists whose sizes (** The function [reshape k l] transforms [l] into a list of lists whose sizes
...@@ -217,8 +217,8 @@ Inductive zipped_Forall {A} (P : list A → list A → A → Prop) : ...@@ -217,8 +217,8 @@ Inductive zipped_Forall {A} (P : list A → list A → A → Prop) :
| zipped_Forall_nil l : zipped_Forall P l [] | zipped_Forall_nil l : zipped_Forall P l []
| zipped_Forall_cons l k x : | zipped_Forall_cons l k x :
P l k x zipped_Forall P (x :: l) k zipped_Forall P l (x :: k). P l k x zipped_Forall P (x :: l) k zipped_Forall P l (x :: k).
Arguments zipped_Forall_nil {_ _} _. Arguments zipped_Forall_nil {_ _} _ : assert.
Arguments zipped_Forall_cons {_ _} _ _ _ _ _. Arguments zipped_Forall_cons {_ _} _ _ _ _ _ : assert.
(** The function [mask f βs l] applies the function [f] to elements in [l] at (** The function [mask f βs l] applies the function [f] to elements in [l] at
positions that are [true] in [βs]. *) positions that are [true] in [βs]. *)
...@@ -3504,9 +3504,9 @@ over the type of constants, but later we use [nat]s and a list representing ...@@ -3504,9 +3504,9 @@ over the type of constants, but later we use [nat]s and a list representing
a corresponding environment. *) a corresponding environment. *)
Inductive rlist (A : Type) := Inductive rlist (A : Type) :=
rnil : rlist A | rnode : A rlist A | rapp : rlist A rlist A rlist A. rnil : rlist A | rnode : A rlist A | rapp : rlist A rlist A rlist A.
Arguments rnil {_}. Arguments rnil {_} : assert.
Arguments rnode {_} _. Arguments rnode {_} _ : assert.
Arguments rapp {_} _ _. Arguments rapp {_} _ _ : assert.
Module rlist. Module rlist.
Fixpoint to_list {A} (t : rlist A) : list A := Fixpoint to_list {A} (t : rlist A) : list A :=
......
...@@ -6,8 +6,8 @@ From stdpp Require Export collections list. ...@@ -6,8 +6,8 @@ From stdpp Require Export collections list.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Record listset A := Listset { listset_car: list A }. Record listset A := Listset { listset_car: list A }.
Arguments listset_car {_} _. Arguments listset_car {_} _ : assert.
Arguments Listset {_} _. Arguments Listset {_} _ : assert.
Section listset. Section listset.
Context {A : Type}. Context {A : Type}.
......
...@@ -9,9 +9,9 @@ Set Default Proof Using "Type". ...@@ -9,9 +9,9 @@ Set Default Proof Using "Type".
Record listset_nodup A := ListsetNoDup { Record listset_nodup A := ListsetNoDup {
listset_nodup_car : list A; listset_nodup_prf : NoDup listset_nodup_car listset_nodup_car : list A; listset_nodup_prf : NoDup listset_nodup_car
}. }.
Arguments ListsetNoDup {_} _ _. Arguments ListsetNoDup {_} _ _ : assert.
Arguments listset_nodup_car {_} _. Arguments listset_nodup_car {_} _ : assert.
Arguments listset_nodup_prf {_} _. Arguments listset_nodup_prf {_} _ : assert.
Section list_collection. Section list_collection.
Context `{EqDecision A}. Context `{EqDecision A}.
......
...@@ -8,8 +8,8 @@ From stdpp Require Export fin_map_dom. ...@@ -8,8 +8,8 @@ From stdpp Require Export fin_map_dom.
Record mapset (M : Type Type) : Type := Record mapset (M : Type Type) : Type :=
Mapset { mapset_car: M (unit : Type) }. Mapset { mapset_car: M (unit : Type) }.
Arguments Mapset {_} _. Arguments Mapset {_} _ : assert.
Arguments mapset_car {_} _. Arguments mapset_car {_} _ : assert.
Section mapset. Section mapset.
Context `{FinMap K M}. Context `{FinMap K M}.
...@@ -143,4 +143,5 @@ Hint Extern 1 (Difference (mapset _)) => ...@@ -143,4 +143,5 @@ Hint Extern 1 (Difference (mapset _)) =>
eapply @mapset_difference : typeclass_instances. eapply @mapset_difference : typeclass_instances.
Hint Extern 1 (Elements _ (mapset _)) => Hint Extern 1 (Elements _ (mapset _)) =>
eapply @mapset_elems : typeclass_instances. eapply @mapset_elems : typeclass_instances.
Arguments mapset_eq_dec _ _ _ _ : simpl never.
Arguments mapset_eq_dec : simpl never.
...@@ -28,9 +28,9 @@ Record natmap (A : Type) : Type := NatMap { ...@@ -28,9 +28,9 @@ Record natmap (A : Type) : Type := NatMap {
natmap_car : natmap_raw A; natmap_car : natmap_raw A;
natmap_prf : natmap_wf natmap_car natmap_prf : natmap_wf natmap_car
}. }.
Arguments NatMap {_} _ _. Arguments NatMap {_} _ _ : assert.
Arguments natmap_car {_} _. Arguments natmap_car {_} _ : assert.
Arguments natmap_prf {_} _. Arguments natmap_prf {_} _ : assert.
Lemma natmap_eq {A} (m1 m2 : natmap A) : Lemma natmap_eq {A} (m1 m2 : natmap A) :
m1 = m2 natmap_car m1 = natmap_car m2. m1 = m2 natmap_car m1 = natmap_car m2.
Proof. Proof.
......
...@@ -9,9 +9,9 @@ Set Default Proof Using "Type". ...@@ -9,9 +9,9 @@ Set Default Proof Using "Type".
Local Open Scope N_scope. Local Open Scope N_scope.
Record Nmap (A : Type) : Type := NMap { Nmap_0 : option A; Nmap_pos : Pmap A }. Record Nmap (A : Type) : Type := NMap { Nmap_0 : option A; Nmap_pos : Pmap A }.
Arguments Nmap_0 {_} _. Arguments Nmap_0 {_} _ : assert.
Arguments Nmap_pos {_} _. Arguments Nmap_pos {_} _ : assert.
Arguments NMap {_} _ _. Arguments NMap {_} _ _ : assert.
Instance Nmap_eq_dec `{EqDecision A} : EqDecision (Nmap A). Instance Nmap_eq_dec `{EqDecision A} : EqDecision (Nmap A).
Proof. Proof.
......
...@@ -14,7 +14,7 @@ Instance comparison_eq_dec : EqDecision comparison. ...@@ -14,7 +14,7 @@ Instance comparison_eq_dec : EqDecision comparison.
Proof. solve_decision. Defined. Proof. solve_decision. Defined.
(** * Notations and properties of [nat] *) (** * Notations and properties of [nat] *)
Arguments minus !_ !_ /. Arguments minus !_ !_ / : assert.
Reserved Notation "x ≤ y ≤ z" (at level 70, y at next level). Reserved Notation "x ≤ y ≤ z" (at level 70, y at next level).
Reserved Notation "x ≤ y < z" (at level 70, y at next level). Reserved Notation "x ≤ y < z" (at level 70, y at next level).
Reserved Notation "x < y < z" (at level 70, y at next level). Reserved Notation "x < y < z" (at level 70, y at next level).
...@@ -212,7 +212,7 @@ Notation "(<)" := N.lt (only parsing) : N_scope. ...@@ -212,7 +212,7 @@ Notation "(<)" := N.lt (only parsing) : N_scope.
Infix "`div`" := N.div (at level 35) : N_scope. Infix "`div`" := N.div (at level 35) : N_scope.
Infix "`mod`" := N.modulo (at level 35) : N_scope. Infix "`mod`" := N.modulo (at level 35) : N_scope.
Arguments N.add _ _ : simpl never. Arguments N.add : simpl never.
Instance Npos_inj : Inj (=) (=) Npos. Instance Npos_inj : Inj (=) (=) Npos.
Proof. by injection 1. Qed. Proof. by injection 1. Qed.
...@@ -281,15 +281,15 @@ Qed. ...@@ -281,15 +281,15 @@ Qed.
(* Note that we cannot disable simpl for [Z.of_nat] as that would break (* Note that we cannot disable simpl for [Z.of_nat] as that would break
tactics as [lia]. *) tactics as [lia]. *)
Arguments Z.to_nat _ : simpl never. Arguments Z.to_nat : simpl never.
Arguments Z.mul _ _ : simpl never. Arguments Z.mul : simpl never.
Arguments Z.add _ _ : simpl never. Arguments Z.add : simpl never.
Arguments Z.opp _ : simpl never. Arguments Z.opp : simpl never.
Arguments Z.pow _ _ : simpl never. Arguments Z.pow : simpl never.
Arguments Z.div _ _ : simpl never. Arguments Z.div : simpl never.
Arguments Z.modulo _ _ : simpl never. Arguments Z.modulo : simpl never.
Arguments Z.quot _ _ : simpl never. Arguments Z.quot : simpl never.
Arguments Z.rem _ _ : simpl never. Arguments Z.rem : simpl never.
Lemma Z_to_nat_neq_0_pos x : Z.to_nat x 0%nat 0 < x. Lemma Z_to_nat_neq_0_pos x : Z.to_nat x 0%nat 0 < x.
Proof. by destruct x. Qed. Proof. by destruct x. Qed.
...@@ -362,7 +362,7 @@ Notation "(≤)" := Qcle (only parsing) : Qc_scope. ...@@ -362,7 +362,7 @@ Notation "(≤)" := Qcle (only parsing) : Qc_scope.
Notation "(<)" := Qclt (only parsing) : Qc_scope. Notation "(<)" := Qclt (only parsing) : Qc_scope.
Hint Extern 1 (_ _) => reflexivity || discriminate. Hint Extern 1 (_ _) => reflexivity || discriminate.
Arguments Qred _ : simpl never. Arguments Qred : simpl never.
Instance Qc_eq_dec: EqDecision Qc := Qc_eq_dec. Instance Qc_eq_dec: EqDecision Qc := Qc_eq_dec.
Program Instance Qc_le_dec (x y : Qc) : Decision (x y) := Program Instance Qc_le_dec (x y : Qc) : Decision (x y) :=
...@@ -512,7 +512,7 @@ Record Qp := mk_Qp { Qp_car :> Qc ; Qp_prf : (0 < Qp_car)%Qc }. ...@@ -512,7 +512,7 @@ Record Qp := mk_Qp { Qp_car :> Qc ; Qp_prf : (0 < Qp_car)%Qc }.
Hint Resolve Qp_prf. Hint Resolve Qp_prf.
Delimit Scope Qp_scope with Qp. Delimit Scope Qp_scope with Qp.
Bind Scope Qp_scope with Qp. Bind Scope Qp_scope with Qp.
Arguments Qp_car _%Qp. Arguments Qp_car _%Qp : assert.
Definition Qp_one : Qp := mk_Qp 1 eq_refl. Definition Qp_one : Qp := mk_Qp 1 eq_refl.
Program Definition Qp_plus (x y : Qp) : Qp := mk_Qp (x + y) _. Program Definition Qp_plus (x y : Qp) : Qp := mk_Qp (x + y) _.
......
...@@ -24,7 +24,7 @@ Proof. congruence. Qed. ...@@ -24,7 +24,7 @@ Proof. congruence. Qed.
Definition from_option {A B} (f : A B) (y : B) (mx : option A) : B := Definition from_option {A B} (f : A B) (y : B) (mx : option A) : B :=
match mx with None => y | Some x => f x end. match mx with None => y | Some x => f x end.
Instance: Params (@from_option) 3. Instance: Params (@from_option) 3.
Arguments from_option {_ _} _ _ !_ /. Arguments from_option {_ _} _ _ !_ / : assert.
(* The eliminator again, but with the arguments in different order, which is (* The eliminator again, but with the arguments in different order, which is
sometimes more convenient. *) sometimes more convenient. *)
...@@ -246,27 +246,27 @@ Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed. ...@@ -246,27 +246,27 @@ Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed.
not particularly like type level reductions. *) not particularly like type level reductions. *)
Class Maybe {A B : Type} (c : A B) := Class Maybe {A B : Type} (c : A B) :=
maybe : B option A. maybe : B option A.
Arguments maybe {_ _} _ {_} !_ /. Arguments maybe {_ _} _ {_} !_ / : assert.
Class Maybe2 {A1 A2 B : Type} (c : A1 A2 B) := Class Maybe2 {A1 A2 B : Type} (c : A1 A2 B) :=
maybe2 : B option (A1 * A2). maybe2 : B option (A1 * A2).
Arguments maybe2 {_ _ _} _ {_} !_ /. Arguments maybe2 {_ _ _} _ {_} !_ / : assert.
Class Maybe3 {A1 A2 A3 B : Type} (c : A1 A2 A3 B) := Class Maybe3 {A1 A2 A3 B : Type} (c : A1 A2 A3 B) :=
maybe3 : B option (A1 * A2 * A3). maybe3 : B option (A1 * A2 * A3).
Arguments maybe3 {_ _ _ _} _ {_} !_ /. Arguments maybe3 {_ _ _ _} _ {_} !_ / : assert.
Class Maybe4 {A1 A2 A3 A4 B : Type} (c : A1 A2 A3 A4 B) := Class Maybe4 {A1 A2 A3 A4 B : Type} (c : A1 A2 A3 A4 B) :=
maybe4 : B option (A1 * A2 * A3 * A4). maybe4 : B option (A1 * A2 * A3 * A4).
Arguments maybe4 {_ _ _ _ _} _ {_} !_ /. Arguments maybe4 {_ _ _ _ _} _ {_} !_ / : assert.
Instance maybe_comp `{Maybe B C c1, Maybe A B c2} : Maybe (c1 c2) := λ x, Instance maybe_comp `{Maybe B C c1, Maybe A B c2} : Maybe (c1 c2) := λ x,
maybe c1 x = maybe c2. maybe c1 x = maybe c2.
Arguments maybe_comp _ _ _ _ _ _ _ !_ /. Arguments maybe_comp _ _ _ _ _ _ _ !_ / : assert.
Instance maybe_inl {A B} : Maybe (@inl A B) := λ xy, Instance maybe_inl {A B} : Maybe (@inl A B) := λ xy,
match xy with inl x => Some x | _ => None end. match xy with inl x => Some x | _ => None end.
Instance maybe_inr {A B} : Maybe (@inr A B) := λ xy, Instance maybe_inr {A B} : Maybe (@inr A B) := λ xy,
match xy with inr y => Some y | _ => None end. match xy with inr y => Some y | _ => None end.
Instance maybe_Some {A} : Maybe (@Some A) := id. Instance maybe_Some {A} : Maybe (@Some A) := id.
Arguments maybe_Some _ !_ /. Arguments maybe_Some _ !_ / : assert.
(** * Union, intersection and difference *) (** * Union, intersection and difference *)
Instance option_union_with {A} : UnionWith A (option A) := λ f mx my, Instance option_union_with {A} : UnionWith A (option A) := λ f mx my,
......
...@@ -24,8 +24,8 @@ all nodes. *) ...@@ -24,8 +24,8 @@ all nodes. *)
Inductive Pmap_raw (A : Type) : Type := Inductive Pmap_raw (A : Type) : Type :=
| PLeaf: Pmap_raw A | PLeaf: Pmap_raw A
| PNode: option A Pmap_raw A Pmap_raw A Pmap_raw A. | PNode: option A Pmap_raw A Pmap_raw A Pmap_raw A.
Arguments PLeaf {_}. Arguments PLeaf {_} : assert.
Arguments PNode {_} _ _ _. Arguments PNode {_} _ _ _ : assert.
Instance Pmap_raw_eq_dec `{EqDecision A} : EqDecision (Pmap_raw A). Instance Pmap_raw_eq_dec `{EqDecision A} : EqDecision (Pmap_raw A).
Proof. solve_decision. Defined. Proof. solve_decision. Defined.
...@@ -36,7 +36,7 @@ Fixpoint Pmap_wf {A} (t : Pmap_raw A) : bool := ...@@ -36,7 +36,7 @@ Fixpoint Pmap_wf {A} (t : Pmap_raw A) : bool :=
| PNode None PLeaf PLeaf => false | PNode None PLeaf PLeaf => false
| PNode _ l r => Pmap_wf l && Pmap_wf r | PNode _ l r => Pmap_wf l && Pmap_wf r
end. end.
Arguments Pmap_wf _ !_ / : simpl nomatch. Arguments Pmap_wf _ !_ / : simpl nomatch, assert.
Lemma Pmap_wf_l {A} o (l r : Pmap_raw A) : Pmap_wf (PNode o l r) Pmap_wf l. Lemma Pmap_wf_l {A} o (l r : Pmap_raw A) : Pmap_wf (PNode o l r) Pmap_wf l.
Proof. destruct o, l, r; simpl; rewrite ?andb_True; tauto. Qed. Proof. destruct o, l, r; simpl; rewrite ?andb_True; tauto. Qed.
Lemma Pmap_wf_r {A} o (l r : Pmap_raw A) : Pmap_wf (PNode o l r) Pmap_wf r. Lemma Pmap_wf_r {A} o (l r : Pmap_raw A) : Pmap_wf (PNode o l r) Pmap_wf r.
...@@ -44,7 +44,7 @@ Proof. destruct o, l, r; simpl; rewrite ?andb_True; tauto. Qed. ...@@ -44,7 +44,7 @@ Proof. destruct o, l, r; simpl; rewrite ?andb_True; tauto. Qed.
Local Hint Immediate Pmap_wf_l Pmap_wf_r. Local Hint Immediate Pmap_wf_l Pmap_wf_r.
Definition PNode' {A} (o : option A) (l r : Pmap_raw A) := Definition PNode' {A} (o : option A) (l r : Pmap_raw A) :=
match l, o, r with PLeaf, None, PLeaf => PLeaf | _, _, _ => PNode o l r end. match l, o, r with PLeaf, None, PLeaf => PLeaf | _, _, _ => PNode o l r end.
Arguments PNode' _ _ _ _ : simpl never. Arguments PNode' : simpl never.
Lemma PNode_wf {A} o (l r : Pmap_raw A) : Lemma PNode_wf {A} o (l r : Pmap_raw A) :
Pmap_wf l Pmap_wf r Pmap_wf (PNode' o l r). Pmap_wf l Pmap_wf r Pmap_wf (PNode' o l r).
Proof. destruct o, l, r; simpl; auto. Qed. Proof. destruct o, l, r; simpl; auto. Qed.
...@@ -59,7 +59,7 @@ Instance Plookup_raw {A} : Lookup positive A (Pmap_raw A) := ...@@ -59,7 +59,7 @@ Instance Plookup_raw {A} : Lookup positive A (Pmap_raw A) :=
| PLeaf => None | PLeaf => None
| PNode o l r => match i with 1 => o | i~0 => l !! i | i~1 => r !! i end | PNode o l r => match i with 1 => o | i~0 => l !! i | i~1 => r !! i end
end. end.
Local Arguments lookup _ _ _ _ _ !_ / : simpl nomatch. Local Arguments lookup _ _ _ _ _ !_ / : simpl nomatch, assert.
Fixpoint Psingleton_raw {A} (i : positive) (x : A) : Pmap_raw A := Fixpoint Psingleton_raw {A} (i : positive) (x : A) : Pmap_raw A :=
match i with match i with
| 1 => PNode (Some x) PLeaf PLeaf | 1 => PNode (Some x) PLeaf PLeaf
...@@ -258,9 +258,9 @@ Qed. ...@@ -258,9 +258,9 @@ Qed.
(** Packed version and instance of the finite map type class *) (** Packed version and instance of the finite map type class *)
Inductive Pmap (A : Type) : Type := Inductive Pmap (A : Type) : Type :=
PMap { pmap_car : Pmap_raw A; pmap_prf : Pmap_wf pmap_car }. PMap { pmap_car : Pmap_raw A; pmap_prf : Pmap_wf pmap_car }.
Arguments PMap {_} _ _. Arguments PMap {_} _ _ : assert.
Arguments pmap_car {_} _. Arguments pmap_car {_} _ : assert.
Arguments pmap_prf {_} _. Arguments pmap_prf {_} _ : assert.
Lemma Pmap_eq {A} (m1 m2 : Pmap A) : m1 = m2 pmap_car m1 = pmap_car m2. Lemma Pmap_eq {A} (m1 m2 : Pmap A) : m1 = m2 pmap_car m1 = pmap_car m2.
Proof. Proof.
split; [by intros ->|intros]; destruct m1 as [t1 ?], m2 as [t2 ?]. split; [by intros ->|intros]; destruct m1 as [t1 ?], m2 as [t2 ?].
......
...@@ -6,8 +6,8 @@ Set Default Proof Using "Type". ...@@ -6,8 +6,8 @@ Set Default Proof Using "Type".