Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Adapt to coq#pr19611 #45

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Adapt to coq#pr19611 #45

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions core/finmap.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1056,7 +1056,7 @@ Section MapDef.
Variables (A B : ordType) (V : Type).

Variable (f: A -> B).
Hypothesis Hf : forall x y, strictly_increasing f x y.
Hypothesis Hf : forall x y, @strictly_increasing A B f x y.

Definition mapk (m : finMap A V) : finMap B V :=
foldfmap (fun p s => ins (f (key p)) (value p) s) nil m.
Expand Down Expand Up @@ -1087,15 +1087,15 @@ End MapDef.
Arguments mapk {A B V} f m.

Variables (A B C : ordType) (V : Type) (f : A -> B) (g : B -> C).
Hypothesis Hf : forall x y, strictly_increasing f x y.
Hypothesis Hf : forall x y, @strictly_increasing A B f x y.

Lemma mapk_id m : @mapk A A V id m = m.
Proof.
by elim/fmap_ind': m=>// k v s L IH; rewrite -{2}IH /mapk foldf_ins //.
Qed.

Lemma mapk_comp m:
mapk g (@mapk A B V f m) = mapk (comp g f) m.
@mapk B C V g (mapk f m) = mapk (comp g f) m.
Proof.
elim/fmap_ind': m =>//= k v s P IH.
rewrite [mapk (g \o f) _]mapk_ins //.
Expand Down Expand Up @@ -1134,7 +1134,7 @@ Fixpoint zip' (s1 s2 : seq (K * V)) :=
| _, _ => None
end.

Definition zip_unit' (s : seq (K * V)) := mapf' unit_f s.
Definition zip_unit' (s : seq (K * V)) := @mapf' K _ _ unit_f s.

Lemma zipC' s1 s2 : zip' s1 s2 = zip' s2 s1.
Proof.
Expand Down
28 changes: 14 additions & 14 deletions pcm/automap.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -74,15 +74,15 @@ End ReflectionContexts.
(* now for reflection *)

Section Reflection.
Variables (K : ordType) (C : pred K) (T : Type) (U : union_map C T).
Implicit Type i : ctx U.
Variables (K : ordType) (C : pred K) (T : Type) (U : @union_map K C T).
Implicit Type i : @ctx K _ _ U.

Inductive term := Pts of nat & T | Var of nat.

(* interpretation function for elements *)
(* interpretjtion function for elements *)
Definition interp' i t :=
match t with
Pts n v => if onth (keyx i) n is Some k then pts k v else undef
Pts n v => if onth (keyx i) n is Some k then @pts K _ _ _ k v else undef
| Var n => if onth (varx i) n is Some f then f else undef
end.

Expand Down Expand Up @@ -200,7 +200,7 @@ End Reflection.
(* subterm is purely functional version of validX *)

Section Subterm.
Variables (K : ordType) (C : pred K) (T : Type) (U : union_map C T).
Variables (K : ordType) (C : pred K) (T : Type) (U : @union_map K C T).
Implicit Types (i : ctx U) (ts : seq (term T)).

Fixpoint subterm ts1 ts2 :=
Expand Down Expand Up @@ -232,7 +232,7 @@ End Subterm.
(* subtract is purely functional version of domeqX *)

Section Subtract.
Variables (K : ordType) (C : pred K) (T : Type) (U : union_map C T).
Variables (K : ordType) (C : pred K) (T : Type) (U : @union_map K C T).
Implicit Types (i : ctx U) (ts : seq (term T)).

(* We need a subterm lemma that returns the uncancelled stuff from *)
Expand Down Expand Up @@ -273,7 +273,7 @@ End Subtract.
(* invalid is a purely functional test of invalidX *)

Section Invalid.
Variables (K : ordType) (C : pred K) (T : Type) (U : union_map C T).
Variables (K : ordType) (C : pred K) (T : Type) (U : @union_map K C T).
Implicit Types (i : ctx U) (t : term T) (ts : seq (term T)).

Definition undefx i t :=
Expand Down Expand Up @@ -315,7 +315,7 @@ End Invalid.

Module Syntactify.
Section Syntactify.
Variables (K : ordType) (C : pred K) (T : Type) (U : union_map C T).
Variables (K : ordType) (C : pred K) (T : Type) (U : @union_map K C T).
Implicit Types (i : ctx U) (ts : seq (term T)).

(* a tagging structure to control the flow of computation *)
Expand Down Expand Up @@ -404,7 +404,7 @@ Export Syntactify.Exports.

Module ValidX.
Section ValidX.
Variables (K : ordType) (C : pred K) (T : Type) (U : union_map C T).
Variables (K : ordType) (C : pred K) (T : Type) (U : @union_map K C T).
Implicit Types (j : ctx U) (ts : seq (term T)).
Notation form := Syntactify.form.
Notation untag := Syntactify.untag.
Expand Down Expand Up @@ -471,7 +471,7 @@ Canonical equate.
Canonical start.

Section Exports.
Variables (K : ordType) (C : pred K) (T : Type) (U : union_map C T).
Variables (K : ordType) (C : pred K) (T : Type) (U : @union_map K C T).
Implicit Types (j : ctx U) (ts : seq (term T)).
Notation form := Syntactify.form.
Notation untag := Syntactify.untag.
Expand Down Expand Up @@ -509,7 +509,7 @@ Export ValidX.Exports.

Module DomeqX.
Section DomeqX.
Variables (K : ordType) (C : pred K) (T : Type) (U : union_map C T).
Variables (K : ordType) (C : pred K) (T : Type) (U : @union_map K C T).
Implicit Types (j : ctx U) (ts : seq (term T)).
Notation form := Syntactify.form.
Notation untag := Syntactify.untag.
Expand Down Expand Up @@ -548,7 +548,7 @@ Canonical equate.
Canonical start.

Section Exports.
Variables (K : ordType) (C : pred K) (T : Type) (U : union_map C T).
Variables (K : ordType) (C : pred K) (T : Type) (U : @union_map K C T).
Implicit Types (j : ctx U) (ts : seq (term T)).
Notation form := Syntactify.form.
Notation untag := Syntactify.untag.
Expand Down Expand Up @@ -583,7 +583,7 @@ Export DomeqX.Exports.

Module InvalidX.
Section InvalidX.
Variables (K : ordType) (C : pred K) (T : Type) (U : union_map C T).
Variables (K : ordType) (C : pred K) (T : Type) (U : @union_map K C T).
Implicit Types (i : ctx U) (ts : seq (term T)).
Notation form := Syntactify.form.
Notation untag := Syntactify.untag.
Expand Down Expand Up @@ -614,7 +614,7 @@ Canonical equate.
Canonical start.

Section Exports.
Variables (K : ordType) (C : pred K) (T : Type) (U : union_map C T).
Variables (K : ordType) (C : pred K) (T : Type) (U : @union_map K C T).
Implicit Types (i : ctx U) (ts : seq (term T)).
Notation form := Syntactify.form.
Notation untag := Syntactify.untag.
Expand Down
2 changes: 1 addition & 1 deletion pcm/natmap.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2696,7 +2696,7 @@ Variables (V R : Type) (U : natmap V) (X : ordType) (a : R -> V -> R) (f : R ->
Implicit Types p : pred (nat*V).

Definition growing (h : U) :=
forall k v z0, (k, v) \In h -> oleq (f z0) (f (a z0 v)).
forall k v z0, (k, v) \In h -> @oleq X (f z0) (f (a z0 v)).

Lemma growL h1 h2 : valid (h1 \+ h2) -> growing (h1 \+ h2) -> growing h1.
Proof. by move=>W G k v z0 H; apply: (G k); apply/InL. Qed.
Expand Down
Loading