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/coq#18939 (Unification Firstorder Function Conversion off) #93

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

Adapt to coq/coq#18939 (Unification Firstorder Function Conversion off) #93

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
4 changes: 2 additions & 2 deletions BigN/Nbasic.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -322,8 +322,8 @@ Section CompareRec.
Lemma spec_compare0_mn: forall n x,
compare0_mn n x = (0 ?= double_to_Z n x).
Proof.
intros n; elim n; clear n; auto.
intros x; rewrite spec_compare0_m; rewrite w_to_Z_0; auto.
intros n; elim n; clear n.
{ intros. rewrite w_to_Z_0 in spec_compare0_m. exact (spec_compare0_m x). }
intros n Hrec x; case x; unfold compare0_mn; fold compare0_mn; auto.
fold word in *.
intros xh xl.
Expand Down
9 changes: 5 additions & 4 deletions BigN/gen/NMake_gen.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -994,7 +994,7 @@ pr "
inversion LT |
subst; change (reduce 0 x = red_t 0 x); reflexivity |
specialize (H (pred n)); subst; destruct x;
[|unfold_red; rewrite H; auto]; reflexivity
[|unfold_red; simpl in H; rewrite H; auto]; reflexivity
].

Lemma reduce_equiv : forall n x, n <= Size -> reduce n x = red_t n x.
Expand All @@ -1006,9 +1006,10 @@ pr "
Lemma spec_reduce_n : forall n x, [reduce_n n x] = [Nn n x].
Proof.
assert (H : forall x, reduce_%i x = red_t (SizePlus 1) x).
destruct x; [|unfold reduce_%i; rewrite (reduce_equiv Size)]; auto.
(* we have to [change] even though we declared equivalent keys... *)
destruct x; [|unfold reduce_%i; change reduce_%i with (reduce %i); rewrite (reduce_equiv Size)]; auto.
induction n.
intros. rewrite H. apply spec_red_t.
intros. simpl. rewrite H. apply spec_red_t.
destruct x as [|xh xl].
simpl. rewrite make_op_S. exact ZnZ.spec_0.
fold word in *.
Expand All @@ -1017,7 +1018,7 @@ pr "
rewrite IHn.
rewrite spec_extend_WW; auto.
Qed.
" (size+1) (size+1);
" (size+1) (size+1) size size;

pr
" Lemma spec_reduce : forall n x, [reduce n x] = ZnZ.to_Z x.
Expand Down
7 changes: 4 additions & 3 deletions CyclicDouble/DoubleBase.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -367,9 +367,10 @@ Section DoubleBase.
Lemma spec_double_WW : forall n (h l : word w n),
[!S n|double_WW n h l!] = [!n|h!] * double_wB n + [!n|l!].
Proof.
induction n;simpl;intros;trivial.
destruct h;auto.
destruct l;auto.
induction n;simpl;intros.
- unfold ww_to_Z in spec_w_WW; trivial.
- destruct h;auto.
destruct l;auto.
Qed.

Lemma spec_extend_aux : forall n x, [!S n|extend_aux n x!] = [[x]].
Expand Down
Loading