diff options
| author | Brian Campbell | 2020-08-25 18:36:19 +0100 |
|---|---|---|
| committer | Brian Campbell | 2020-08-26 10:34:57 +0100 |
| commit | ce87c17955727a7c2a0178a635c4bd17edd4252c (patch) | |
| tree | dc9af7ded96fa25fde2c75ee482e2233bede107d | |
| parent | ac2d2a9e0115693064d10d38ad8208a0e9f70b43 (diff) | |
Coq: Use proof mode for a couple of Fixpoints to avoid Coq 8.12 issue
| -rw-r--r-- | lib/coq/Values.v | 21 |
1 files changed, 15 insertions, 6 deletions
diff --git a/lib/coq/Values.v b/lib/coq/Values.v index 4b48151a..0119711a 100644 --- a/lib/coq/Values.v +++ b/lib/coq/Values.v @@ -2548,21 +2548,30 @@ Fixpoint foreach_Z' {Vars} from to step n (vars : Vars) (body : Z -> Vars -> Var Definition foreach_Z {Vars} from to step vars body := foreach_Z' (Vars := Vars) from to step (S (Z.abs_nat (from - to))) vars body. -Fixpoint foreach_Z_up' {Vars} (from to step off : Z) (n:nat) `{ArithFact (0 <? step)} `{ArithFact (0 <=? off)} (vars : Vars) (body : forall (z : Z) `(ArithFact ((from <=? z <=? to))), Vars -> Vars) {struct n} : Vars := +(* Define these in proof mode to avoid anomalies related to abstract. + (See https://github.com/coq/coq/issues/10959) *) + +Fixpoint foreach_Z_up' {Vars} (from to step off : Z) (n:nat) `{ArithFact (0 <? step)} `{ArithFact (0 <=? off)} (vars : Vars) (body : forall (z : Z) `(ArithFact ((from <=? z <=? to))), Vars -> Vars) {struct n} : Vars. +refine ( if sumbool_of_bool (from + off <=? to) then match n with | O => vars - | S n => let vars := body (from + off) _ vars in foreach_Z_up' from to step (off + step) n vars body + | S n => let vars := body (from + off) _ vars in foreach_Z_up' _ from to step (off + step) n _ _ vars body end - else vars. + else vars +). +Defined. -Fixpoint foreach_Z_down' {Vars} from to step off n `{ArithFact (0 <? step)} `{ArithFact (off <=? 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact ((to <=? z <=? from))), Vars -> Vars) {struct n} : Vars := +Fixpoint foreach_Z_down' {Vars} from to step off (n:nat) `{ArithFact (0 <? step)} `{ArithFact (off <=? 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact ((to <=? z <=? from))), Vars -> Vars) {struct n} : Vars. +refine ( if sumbool_of_bool (to <=? from + off) then match n with | O => vars - | S n => let vars := body (from + off) _ vars in foreach_Z_down' from to step (off - step) n vars body + | S n => let vars := body (from + off) _ vars in foreach_Z_down' _ from to step (off - step) n _ _ vars body end - else vars. + else vars +). +Defined. Definition foreach_Z_up {Vars} from to step vars body `{ArithFact (0 <? step)} := foreach_Z_up' (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body. |