Commit 02f213ce authored by Robbert Krebbers's avatar Robbert Krebbers

Port to Coq 8.5 beta 2.

The port makes the following notable changes:

* The carrier types of separation algebras and integer environments are no
  longer in Set. Now they have a type at a fixed type level above Set. This
  both works better in 8.5 and makes the formalization more general.
  I have tried putting them at polymorphic type levels, but that increased the
  compilation time by an order of magnitude.
* I am using a custom f_equal tactic written in Ltac to circumvent bug #4069.
  That bug has been fixed, so this custom tactic can be removed when the next
  beta of 8.5 is out.
parent 462ea92a
......@@ -269,7 +269,7 @@ End assoc.
(** * Finite sets *)
(** We construct finite sets using the above implementation of maps. *)
Notation assoc_set K := (mapset (assoc K unit)).
Notation assoc_set K := (mapset (assoc K)).
Instance assoc_map_dom `{Lexico K, !TrichotomyT (@lexico K _),
!StrictOrder lexico} {A} : Dom (assoc K A) (assoc_set K) := mapset_dom.
Instance assoc_map_dom_spec `{Lexico K} `{!TrichotomyT (@lexico K _)}
......
......@@ -6,6 +6,7 @@ abstract interfaces for ordered structures, collections, and various other data
structures. *)
Global Generalizable All Variables.
Global Set Automatic Coercions Import.
Global Set Asymmetric Patterns.
Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid.
(** * General *)
......@@ -418,23 +419,23 @@ Notation "(≫= f )" := (mbind f) (only parsing) : C_scope.
Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : C_scope.
Notation "x ← y ; z" := (y = (λ x : _, z))
(at level 65, next at level 35, only parsing, right associativity) : C_scope.
(at level 65, only parsing, right associativity) : C_scope.
Infix "<$>" := fmap (at level 60, right associativity) : C_scope.
Notation "' ( x1 , x2 ) ← y ; z" :=
(y = (λ x : _, let ' (x1, x2) := x in z))
(at level 65, next at level 35, only parsing, right associativity) : C_scope.
(at level 65, only parsing, right associativity) : C_scope.
Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
(y = (λ x : _, let ' (x1,x2,x3) := x in z))
(at level 65, next at level 35, only parsing, right associativity) : C_scope.
(at level 65, only parsing, right associativity) : C_scope.
Notation "' ( x1 , x2 , x3 , x4 ) ← y ; z" :=
(y = (λ x : _, let ' (x1,x2,x3,x4) := x in z))
(at level 65, next at level 35, only parsing, right associativity) : C_scope.
(at level 65, only parsing, right associativity) : C_scope.
Notation "' ( x1 , x2 , x3 , x4 , x5 ) ← y ; z" :=
(y = (λ x : _, let ' (x1,x2,x3,x4,x5) := x in z))
(at level 65, next at level 35, only parsing, right associativity) : C_scope.
(at level 65, only parsing, right associativity) : C_scope.
Notation "' ( x1 , x2 , x3 , x4 , x5 , x6 ) ← y ; z" :=
(y = (λ x : _, let ' (x1,x2,x3,x4,x5,x6) := x in z))
(at level 65, next at level 35, only parsing, right associativity) : C_scope.
(at level 65, only parsing, right associativity) : C_scope.
Notation "ps .*1" := (fmap (M:=list) fst ps)
(at level 10, format "ps .*1").
......@@ -445,9 +446,9 @@ Class MGuard (M : Type → Type) :=
mguard: P {dec : Decision P} {A}, (P M A) M A.
Arguments mguard _ _ _ !_ _ _ /.
Notation "'guard' P ; o" := (mguard P (λ _, o))
(at level 65, next at level 35, only parsing, right associativity) : C_scope.
(at level 65, only parsing, right associativity) : C_scope.
Notation "'guard' P 'as' H ; o" := (mguard P (λ H, o))
(at level 65, next at level 35, only parsing, right associativity) : C_scope.
(at level 65, only parsing, right associativity) : C_scope.
(** ** Operations on maps *)
(** In this section we define operational type classes for the operations
......
......@@ -109,8 +109,7 @@ Section of_option_list.
Proof.
split.
* induction l; simpl; [by rewrite elem_of_empty|].
rewrite elem_of_union, elem_of_singleton;
intros [->|?]; constructor (auto).
rewrite elem_of_union,elem_of_singleton; intros [->|?]; constructor; auto.
* induction 1; simpl; rewrite elem_of_union, elem_of_singleton; auto.
Qed.
End of_option_list.
......
......@@ -68,7 +68,7 @@ Lemma surjective_cancel `{Countable A} `{∀ x y : B, Decision (x = y)}
(f : A B) `{!Surjective (=) f} : { g : B A & Cancel (=) f g }.
Proof.
exists (λ y, choose (λ x, f x = y) (surjective f y)).
intros y. by rewrite (choose_correct (λ _, _) (surjective f y)).
intros y. by rewrite (choose_correct (λ x, f x = y) (surjective f y)).
Qed.
(** ** Instances *)
......@@ -200,7 +200,7 @@ Program Instance list_countable `{Countable A} : Countable (list A) := {|
decode p := list_decode p = mapM decode
|}.
Next Obligation.
intros ??? l. rewrite list_decode_encode. simpl.
intros ??? l; simpl; rewrite list_decode_encode; simpl.
apply mapM_fmap_Some; auto using decode_encode.
Qed.
......@@ -227,5 +227,5 @@ Program Instance nat_countable : Countable nat := {|
decode p := N.to_nat <$> decode p
|}.
Next Obligation.
intros x. rewrite decode_encode; csimpl. by rewrite Nat2N.id.
intros x; lazy beta; rewrite decode_encode; csimpl. by rewrite Nat2N.id.
Qed.
......@@ -125,13 +125,9 @@ Proof. repeat case_bool_decide; tauto. Qed.
(** Leibniz equality on Sigma types requires the equipped proofs to be
equal as Coq does not support proof irrelevance. For decidable we
propositions we define the type [dsig P] whose Leibniz equality is proof
irrelevant. That is [∀ x y : dsig P, x = y ↔ `x = `y]. Due to the absence of
universe polymorpic definitions we also define a variant [dsigS] for types
in [Set]. *)
irrelevant. That is [∀ x y : dsig P, x = y ↔ `x = `y]. *)
Definition dsig `(P : A Prop) `{ x : A, Decision (P x)} :=
{ x | bool_decide (P x) }.
Definition dsigS {A : Set} (P : A Prop) `{ x : A, Decision (P x)} : Set :=
{ x | bool_decide (P x) }.
Definition proj2_dsig `{ x : A, Decision (P x)} (x : dsig P) : P (`x) :=
bool_decide_unpack _ (proj2_sig x).
......
......@@ -27,7 +27,7 @@ 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, next at level 35, only parsing, right associativity) : C_scope.
(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.
......
......@@ -586,7 +586,7 @@ Proof. destruct l. done. by edestruct 1; constructor. Qed.
Lemma elem_of_not_nil x l : x l l [].
Proof. intros ? ->. by apply (elem_of_nil x). Qed.
Lemma elem_of_cons l x y : x y :: l x = y x l.
Proof. split; [inversion 1; subst|intros [->|?]]; constructor (done). Qed.
Proof. by split; [inversion 1; subst|intros [->|?]]; constructor. Qed.
Lemma not_elem_of_cons l x y : x y :: l x y x l.
Proof. rewrite elem_of_cons. tauto. Qed.
Lemma elem_of_app l1 l2 x : x l1 ++ l2 x l1 x l2.
......@@ -623,8 +623,8 @@ Proof.
split.
* induction l as [|x l]; csimpl; repeat case_match; inversion 1; subst;
setoid_rewrite elem_of_cons; naive_solver.
* intros (x&Hx&?). induction Hx; csimpl; repeat case_match;
simplify_equality; auto; constructor (by auto).
* intros (x&Hx&?). by induction Hx; csimpl; repeat case_match;
simplify_equality; try constructor; auto.
Qed.
(** ** Properties of the [NoDup] predicate *)
......@@ -1311,7 +1311,7 @@ Definition Permutation_skip := @perm_skip A.
Definition Permutation_swap := @perm_swap A.
Definition Permutation_singleton_inj := @Permutation_length_1 A.
Global Existing Instance Permutation_app'_Proper.
Global Existing Instance Permutation_app'.
Global Instance: Proper (() ==> (=)) (@length A).
Proof. induction 1; simpl; auto with lia. Qed.
Global Instance: Commutative () (@app A).
......@@ -2037,7 +2037,7 @@ Section Forall_Exists.
Proof. intros H ?. induction H; auto. Defined.
Global Instance Forall_proper:
Proper (pointwise_relation _ () ==> (=) ==> ()) (@Forall A).
Proof. split; subst; induction 1; constructor (by firstorder auto). Qed.
Proof. split; subst; induction 1; constructor; by firstorder auto. Qed.
Lemma Forall_iff l (Q : A Prop) :
( x, P x Q x) Forall P l Forall Q l.
Proof. intros H. apply Forall_proper. red; apply H. done. Qed.
......@@ -2150,7 +2150,7 @@ Section Forall_Exists.
Proof. intros H ?. induction H; auto. Defined.
Global Instance Exists_proper:
Proper (pointwise_relation _ () ==> (=) ==> ()) (@Exists A).
Proof. split; subst; induction 1; constructor (by firstorder auto). Qed.
Proof. split; subst; induction 1; constructor; by firstorder auto. Qed.
Lemma Exists_not_Forall l : Exists (not P) l ¬Forall P l.
Proof. induction 1; inversion_clear 1; contradiction. Qed.
Lemma Forall_not_Exists l : Forall (not P) l ¬Exists P l.
......@@ -2466,7 +2466,7 @@ Section Forall2_order.
Global Instance: Symmetric R Symmetric (Forall2 R).
Proof. intros. induction 1; constructor; auto. Qed.
Global Instance: Transitive R Transitive (Forall2 R).
Proof. intros ????. apply Forall2_transitive. apply transitivity. Qed.
Proof. intros ????. apply Forall2_transitive. by apply @transitivity. Qed.
Global Instance: Equivalence R Equivalence (Forall2 R).
Proof. split; apply _. Qed.
Global Instance: PreOrder R PreOrder (Forall2 R).
......@@ -2658,7 +2658,7 @@ Section fmap.
Lemma Forall_fmap (P : B Prop) l : Forall P (f <$> l) Forall (P f) l.
Proof. split; induction l; inversion_clear 1; constructor; auto. Qed.
Lemma Exists_fmap (P : B Prop) l : Exists P (f <$> l) Exists (P f) l.
Proof. split; induction l; inversion 1; constructor (by auto). Qed.
Proof. split; induction l; inversion 1; constructor; by auto. Qed.
Lemma Forall2_fmap_l {C} (P : B C Prop) l1 l2 :
Forall2 P (f <$> l1) l2 Forall2 (P f) l1 l2.
Proof.
......
......@@ -5,28 +5,29 @@ elements of the unit type. Since maps enjoy extensional equality, the
constructed finite sets do so as well. *)
Require Export fin_map_dom.
Record mapset (Mu : Type) := Mapset { mapset_car: Mu }.
Record mapset (M : Type Type) : Type :=
Mapset { mapset_car: M (unit : Type) }.
Arguments Mapset {_} _.
Arguments mapset_car {_} _.
Section mapset.
Context `{FinMap K M}.
Instance mapset_elem_of: ElemOf K (mapset (M unit)) := λ x X,
Instance mapset_elem_of: ElemOf K (mapset M) := λ x X,
mapset_car X !! x = Some ().
Instance mapset_empty: Empty (mapset (M unit)) := Mapset .
Instance mapset_singleton: Singleton K (mapset (M unit)) := λ x,
Instance mapset_empty: Empty (mapset M) := Mapset .
Instance mapset_singleton: Singleton K (mapset M) := λ x,
Mapset {[ (x,()) ]}.
Instance mapset_union: Union (mapset (M unit)) := λ X1 X2,
Instance mapset_union: Union (mapset M) := λ X1 X2,
let (m1) := X1 in let (m2) := X2 in Mapset (m1 m2).
Instance mapset_intersection: Intersection (mapset (M unit)) := λ X1 X2,
Instance mapset_intersection: Intersection (mapset M) := λ X1 X2,
let (m1) := X1 in let (m2) := X2 in Mapset (m1 m2).
Instance mapset_difference: Difference (mapset (M unit)) := λ X1 X2,
Instance mapset_difference: Difference (mapset M) := λ X1 X2,
let (m1) := X1 in let (m2) := X2 in Mapset (m1 m2).
Instance mapset_elems: Elements K (mapset (M unit)) := λ X,
Instance mapset_elems: Elements K (mapset M) := λ X,
let (m) := X in (map_to_list m).*1.
Lemma mapset_eq (X1 X2 : mapset (M unit)) : X1 = X2 x, x X1 x X2.
Lemma mapset_eq (X1 X2 : mapset M) : X1 = X2 x, x X1 x X2.
Proof.
split; [by intros ->|].
destruct X1 as [m1], X2 as [m2]. simpl. intros E.
......@@ -34,17 +35,16 @@ Proof.
Qed.
Global Instance mapset_eq_dec `{ m1 m2 : M unit, Decision (m1 = m2)}
(X1 X2 : mapset (M unit)) : Decision (X1 = X2) | 1.
(X1 X2 : mapset M) : Decision (X1 = X2) | 1.
Proof.
refine
match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end;
abstract congruence.
Defined.
Global Instance mapset_elem_of_dec x (X : mapset (M unit)) :
Decision (x X) | 1.
Global Instance mapset_elem_of_dec x (X : mapset M) : Decision (x X) | 1.
Proof. solve_decision. Defined.
Instance: Collection K (mapset (M unit)).
Instance: Collection K (mapset M).
Proof.
split; [split | | ].
* unfold empty, elem_of, mapset_empty, mapset_elem_of.
......@@ -63,9 +63,9 @@ Proof.
intros [m1] [m2] ?. simpl. rewrite lookup_difference_Some.
destruct (m2 !! x) as [[]|]; intuition congruence.
Qed.
Global Instance: PartialOrder (@subseteq (mapset (M unit)) _).
Global Instance: PartialOrder (@subseteq (mapset M) _).
Proof. split; try apply _. intros ????. apply mapset_eq. intuition. Qed.
Global Instance: FinCollection K (mapset (M unit)).
Global Instance: FinCollection K (mapset M).
Proof.
split.
* apply _.
......@@ -78,12 +78,12 @@ Proof.
Qed.
Definition mapset_map_with {A B} (f : bool A option B)
(X : mapset (M unit)) : M A M B :=
(X : mapset M) : M A M B :=
let (mX) := X in merge (λ x y,
match x, y with
| Some _, Some a => f true a | None, Some a => f false a | _, None => None
end) mX.
Definition mapset_dom_with {A} (f : A bool) (m : M A) : mapset (M unit) :=
Definition mapset_dom_with {A} (f : A bool) (m : M A) : mapset M :=
Mapset $ merge (λ x _,
match x with
| Some a => if f a then Some () else None | None => None
......@@ -104,9 +104,8 @@ Proof.
* destruct (Is_true_reflect (f a)); naive_solver.
* naive_solver.
Qed.
Instance mapset_dom {A} : Dom (M A) (mapset (M unit)) :=
mapset_dom_with (λ _, true).
Instance mapset_dom_spec: FinMapDom K M (mapset (M unit)).
Instance mapset_dom {A} : Dom (M A) (mapset M) := mapset_dom_with (λ _, true).
Instance mapset_dom_spec: FinMapDom K M (mapset M).
Proof.
split; try apply _. intros. unfold dom, mapset_dom, is_Some.
rewrite elem_of_mapset_dom_with; naive_solver.
......
......@@ -255,7 +255,7 @@ Proof.
Qed.
(** Finally, we can construct sets of [nat]s satisfying extensional equality. *)
Notation natset := (mapset (natmap unit)).
Notation natset := (mapset natmap).
Instance natmap_dom {A} : Dom (natmap A) natset := mapset_dom.
Instance: FinMapDom nat natmap natset := mapset_dom_spec.
......
......@@ -7,7 +7,7 @@ Require Export prelude fin_maps.
Local Open Scope N_scope.
Record Nmap A := 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_pos {_} _.
Arguments NMap {_} _ _.
......@@ -81,7 +81,7 @@ Qed.
(** * Finite sets *)
(** We construct sets of [N]s satisfying extensional equality. *)
Notation Nset := (mapset (Nmap unit)).
Notation Nset := (mapset Nmap).
Instance Nmap_dom {A} : Dom (Nmap A) Nset := mapset_dom.
Instance: FinMapDom N Nmap Nset := mapset_dom_spec.
......
......@@ -28,8 +28,8 @@ Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z')%nat : nat_
Notation "(≤)" := le (only parsing) : nat_scope.
Notation "(<)" := lt (only parsing) : nat_scope.
Infix "`div`" := NPeano.div (at level 35) : nat_scope.
Infix "`mod`" := NPeano.modulo (at level 35) : nat_scope.
Infix "`div`" := Nat.div (at level 35) : nat_scope.
Infix "`mod`" := Nat.modulo (at level 35) : nat_scope.
Instance nat_eq_dec: x y : nat, Decision (x = y) := eq_nat_dec.
Instance nat_le_dec: x y : nat, Decision (x y) := le_dec.
......
......@@ -80,9 +80,8 @@ Qed.
End optionmap.
(** * Finite sets *)
Notation optionset M := (mapset (optionmap M unit)).
Notation optionset M := (mapset (optionmap M)).
Instance optionmap_dom {M : Type Type} `{ A, Empty (M A), Merge M} {A} :
Dom (optionmap M A) (optionset M) := mapset_dom.
Instance optionmap_domspec `{FinMap K M} :
FinMapDom (option K) (optionmap M) (optionset M) := mapset_dom_spec.
......@@ -18,7 +18,7 @@ Section orders.
Lemma reflexive_eq `{!Reflexive R} X Y : X = Y X Y.
Proof. by intros <-. Qed.
Lemma anti_symmetric_iff `{!PartialOrder R} X Y : X = Y R X Y R Y X.
Proof. intuition (subst; auto). Qed.
Proof. split. by intros ->. by intros [??]; apply (anti_symmetric _). Qed.
Lemma strict_spec X Y : X Y X Y Y X.
Proof. done. Qed.
Lemma strict_include X Y : X Y X Y.
......
......@@ -19,7 +19,7 @@ Local Hint Extern 0 (¬@eq positive _ _) => congruence.
not ensure canonical representations of maps. For example the empty map can
be represented as a binary tree of an arbitrary size that contains [None] at
all nodes. *)
Inductive Pmap_raw A :=
Inductive Pmap_raw (A : Type) : Type :=
| PLeaf: Pmap_raw A
| PNode: Pmap_raw A option A Pmap_raw A Pmap_raw A.
Arguments PLeaf {_}.
......@@ -44,7 +44,7 @@ Proof.
| PLeaf => right _
| PNode _ (Some x) _ => left _
| PNode l Node r => cast_if_or (go l) (go r)
end); clear go; abstract first [constructor (by auto)|by inversion 1].
end); clear go; abstract first [constructor; by auto|by inversion 1].
Defined.
(** The following predicate describes well well formed trees. A tree is well
......@@ -65,12 +65,12 @@ Proof.
| PNode l (Some x) r => cast_if_and (go l) (go r)
| PNode l Node r =>
cast_if_and3 (decide (Pmap_ne l Pmap_ne r)) (go l) (go r)
end); clear go; abstract first [constructor (by auto)|by inversion 1].
end); clear go; abstract first [constructor; by auto|by inversion 1].
Defined.
(** Now we restrict the data type of trees to those that are well formed and
thereby obtain a data type that ensures canonicity. *)
Inductive Pmap A := PMap {
Inductive Pmap (A : Type) : Type := PMap {
pmap_car : Pmap_raw A;
pmap_bool_prf : bool_decide (Pmap_wf pmap_car)
}.
......@@ -387,7 +387,7 @@ Qed.
(** * Finite sets *)
(** We construct sets of [positives]s satisfying extensional equality. *)
Notation Pset := (mapset (Pmap unit)).
Notation Pset := (mapset Pmap).
Instance Pmap_dom {A} : Dom (Pmap A) Pset := mapset_dom.
Instance: FinMapDom positive Pmap Pset := mapset_dom_spec.
......
......@@ -18,40 +18,54 @@ Definition pretty_N_char (x : N) : ascii :=
| 0 => "0" | 1 => "1" | 2 => "2" | 3 => "3" | 4 => "4"
| 5 => "5" | 6 => "6" | 7 => "7" | 8 => "8" | _ => "9"
end%char%N.
Definition pretty_N_go (x : N)
(go : y, (y < x)%N string string) (s : string) : string :=
Fixpoint pretty_N_go_help (x : N) (acc : Acc (<)%N x) (s : string) : string :=
match decide (0 < x)%N with
| left H => go (x `div` 10)%N (N.div_lt x 10 H eq_refl)
| left H => pretty_N_go_help (x `div` 10)%N
(Acc_inv acc (N.div_lt x 10 H eq_refl))
(String (pretty_N_char (x `mod` 10)) s)
| right _ => s
end.
Instance pretty_N : Pretty N := λ x,
Fix_F _ pretty_N_go (wf_guard 32 N.lt_wf_0 x) ""%string.
Definition pretty_N_go (x : N) : string string :=
pretty_N_go_help x (wf_guard 32 N.lt_wf_0 x).
Lemma pretty_N_go_0 s : pretty_N_go 0 s = s.
Proof. done. Qed.
Lemma pretty_N_go_help_irrel x acc1 acc2 s :
pretty_N_go_help x acc1 s = pretty_N_go_help x acc2 s.
Proof.
revert x acc1 acc2 s; fix 2; intros x [acc1] [acc2] s; simpl.
destruct (decide (0 < x)%N); auto.
Qed.
Lemma pretty_N_go_step x s :
(0 < x)%N pretty_N_go x s
= pretty_N_go (x `div` 10) (String (pretty_N_char (x `mod` 10)) s).
Proof.
unfold pretty_N_go; intros; destruct (wf_guard 32 N.lt_wf_0 x).
unfold pretty_N_go_help; fold pretty_N_go_help.
by destruct (decide (0 < x)%N); auto using pretty_N_go_help_irrel.
Qed.
Instance pretty_N : Pretty N := λ x, pretty_N_go x ""%string.
Instance pretty_N_injective : Injective (@eq N) (=) pretty.
Proof.
assert ( x y, x < 10 y < 10
pretty_N_char x = pretty_N_char y x = y)%N.
{ compute; intros. by repeat (discriminate || case_match). }
set (f x (acc : Acc _ x) := Fix_F _ pretty_N_go acc).
cut ( x acc y acc' s s', length s = length s'
f x acc s = f y acc' s' x = y s = s').
cut ( x y s s', pretty_N_go x s = pretty_N_go y s'
length s = length s' x = y s = s').
{ intros help x y ?. eapply help; eauto. }
assert ( x acc s, ¬length (f x acc s) < length s) as help.
assert ( x s, ¬length (pretty_N_go x s) < length s) as help.
{ setoid_rewrite <-Nat.le_ngt.
fix 2; intros x [?] s; simpl. unfold pretty_N_go; fold pretty_N_go.
destruct (decide (0 < x))%N; [|auto].
etransitivity; [|eauto]. simpl; lia. }
fix 2; intros x [?] y [?] s s' ?; simpl.
unfold pretty_N_go; fold pretty_N_go; intros Hs.
destruct (decide (0 < x))%N, (decide (0 < y))%N;
try match goal with
| H : f ?x ?acc ?s = _ |- _ =>
destruct (help x acc s); rewrite H; simpl; lia
| H : _ = f ?x ?acc ?s |- _ =>
destruct (help x acc s); rewrite <-H; simpl; lia
end; auto with lia.
apply pretty_N_injective in Hs; [|by f_equal']; destruct Hs.
simplify_equality; split; [|done].
intros x; induction (N.lt_wf_0 x) as [x _ IH]; intros s.
assert (x = 0 0 < x)%N as [->|?] by lia; [by rewrite pretty_N_go_0|].
rewrite pretty_N_go_step by done.
etransitivity; [|by eapply IH, N.div_lt]; simpl; lia. }
intros x; induction (N.lt_wf_0 x) as [x _ IH]; intros y s s'.
assert ((x = 0 0 < x) (y = 0 0 < y))%N as [[->|?] [->|?]] by lia;
rewrite ?pretty_N_go_0, ?pretty_N_go_step, ?(pretty_N_go_step y) by done.
{ done. }
{ intros -> Hlen; edestruct help; rewrite Hlen; simpl; lia. }
{ intros <- Hlen; edestruct help; rewrite <-Hlen; simpl; lia. }
intros Hs Hlen; apply IH in Hs; destruct Hs;
simplify_equality'; split_ands'; auto using N.div_lt_upper_bound with lia.
rewrite (N.div_mod x 10), (N.div_mod y 10) by done.
auto using N.mod_lt with f_equal.
Qed.
......
......@@ -158,7 +158,7 @@ Qed.
(** * Finite sets *)
(** We construct sets of [strings]s satisfying extensional equality. *)
Notation stringset := (mapset (stringmap unit)).
Notation stringset := (mapset stringmap).
Instance stringmap_dom {A} : Dom (stringmap A) stringset := mapset_dom.
Instance: FinMapDom positive Pmap Pset := mapset_dom_spec.
......
......@@ -5,6 +5,19 @@ the development. *)
Require Export Psatz.
Require Export base.
Lemma f_equal_dep {A B} (f g : x : A, B x) x : f = g f x = g x.
Proof. intros ->; reflexivity. Qed.
Lemma f_equal_help {A B} (f g : A B) x y : f = g x = y f x = g y.
Proof. intros -> ->; reflexivity. Qed.
Ltac f_equal :=
let rec go :=
match goal with
| _ => reflexivity
| _ => apply f_equal_help; [go|try reflexivity]
| |- ?f ?x = ?g ?x => apply (f_equal_dep f g); go
end in
try go.
(** We declare hint databases [f_equal], [congruence] and [lia] and containing
solely the tactic corresponding to its name. These hint database are useful in
to be combined in combination with other hint database. *)
......
......@@ -6,7 +6,7 @@ Require Import pmap mapset.
Require Export prelude fin_maps.
Local Open Scope Z_scope.
Record Zmap A :=
Record Zmap (A : Type) : Type :=
ZMap { Zmap_0 : option A; Zmap_pos : Pmap A; Zmap_neg : Pmap A }.
Arguments Zmap_0 {_} _.
Arguments Zmap_pos {_} _.
......@@ -92,6 +92,6 @@ Qed.
(** * Finite sets *)
(** We construct sets of [Z]s satisfying extensional equality. *)
Notation Zset := (mapset (Zmap unit)).
Notation Zset := (mapset Zmap).
Instance Zmap_dom {A} : Dom (Zmap A) Zset := mapset_dom.
Instance: FinMapDom Z Zmap Zset := mapset_dom_spec.
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