aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Cyclic
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-12-10 19:52:51 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-06-18 13:09:16 +0200
commit1744e371d8fa2a612e3906c643fb5558a54a484f (patch)
tree90bacb89fac6effabc1ca8d205beaa64547cbffc /theories/Numbers/Cyclic
parent2cb554aa772c5c6d179c6a4611b70d459073a316 (diff)
Giving a more natural semantics to injection by default.
There were three versions of injection: 1. "injection term" without "as" clause: was leaving hypotheses on the goal in reverse order 2. "injection term as ipat", first version: was introduction hypotheses using ipat in reverse order without checking that the number of ipat was the size of the injection (activated with "Unset Injection L2R Pattern Order") 3. "injection term as ipat", second version: was introduction hypotheses using ipat in left-to-right order checking that the number of ipat was the size of the injection and clearing the injecting term by default if an hypothesis (activated with "Set Injection L2R Pattern Order", default one from 8.5) There is now: 4. "injection term" without "as" clause, new version: introducing the components of the injection in the context in left-to-right order using default intro-patterns "?" and clearing the injecting term by default if an hypothesis (activated with "Set Structural Injection") The new versions 3. and 4. are the "expected" ones in the sense that they have the following good properties: - introduction in the context is in the natural left-to-right order - "injection" behaves the same with and without "as", always introducing the hypotheses in the goal what corresponds to the natural expectation as the changes I made in the proof scripts for adaptation confirm - clear the "injection" hypothesis when an hypothesis which is the natural expectation as the changes I made in the proof scripts for adaptation confirm The compatibility can be preserved by "Unset Structural Injection" or by calling "simple injection". The flag is currently off.
Diffstat (limited to 'theories/Numbers/Cyclic')
-rw-r--r--theories/Numbers/Cyclic/ZModulo/ZModulo.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
index c115a831d..04fc5a8df 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -369,7 +369,7 @@ Section ZModulo.
assert (Z.div_eucl ([|x|]*[|y|]) wB = (([|x|]*[|y|])/wB,([|x|]*[|y|]) mod wB)).
unfold Z.modulo, Z.div; destruct Z.div_eucl; auto.
generalize (Z_div_mod ([|x|]*[|y|]) wB wB_pos); destruct Z.div_eucl as (h,l).
- destruct 1; injection H; clear H; intros.
+ destruct 1; injection H as ? ?.
rewrite H0.
assert ([|l|] = l).
apply Zmod_small; auto.
@@ -411,7 +411,7 @@ Section ZModulo.
unfold Z.modulo, Z.div; destruct Z.div_eucl; auto.
generalize (Z_div_mod [|a|] [|b|] H0).
destruct Z.div_eucl as (q,r); destruct 1; intros.
- injection H1; clear H1; intros.
+ injection H1 as ? ?.
assert ([|r|]=r).
apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|];
auto with zarith.
@@ -522,7 +522,7 @@ Section ZModulo.
unfold Z.modulo, Z.div; destruct Z.div_eucl; auto.
generalize (Z_div_mod a [|b|] H3).
destruct Z.div_eucl as (q,r); destruct 1; intros.
- injection H4; clear H4; intros.
+ injection H4 as ? ?.
assert ([|r|]=r).
apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|];
auto with zarith.