-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathSsromega.v
33 lines (28 loc) · 1.18 KB
/
Ssromega.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
From Coq Require Import ssreflect ssrfun ssrbool Omega.
Require Import mathcomp.ssreflect.eqtype.
Require Import mathcomp.ssreflect.seq.
Require Import mathcomp.ssreflect.ssrnat.
(* Taken from http://github.com/pi8027/formalized-postscript/blob/master/stdlib_ext.v *)
Ltac arith_hypo_ssrnat2coqnat :=
match goal with
| H : context [andb _ _] |- _ => let H0 := fresh in case/andP: H => H H0
| H : context [orb _ _] |- _ => case/orP: H => H
| H : context [?L <= ?R] |- _ => move/leP: H => H
| H : context [?L < ?R] |- _ => move/ltP : H => H
| H : context [?L == ?R] |- _ => move/eqP : H => H
| H : context [addn ?L ?R] |- _ => rewrite -plusE in H
| H : context [muln ?L ?R] |- _ => rewrite -multE in H
| H : context [subn ?L ?R] |- _ => rewrite -minusE in H
end.
Ltac arith_goal_ssrnat2coqnat :=
rewrite ?NatTrec.trecE -?plusE -?minusE -?multE -?leqNgt -?ltnNge;
repeat match goal with
| |- is_true (andb _ _) => apply/andP; split
| |- is_true (orb _ _) => try apply/orP
| |- is_true (_ <= _) => try apply/leP
| |- is_true (_ < _) => try apply/ltP
end.
Ltac ssromega :=
repeat arith_hypo_ssrnat2coqnat;
arith_goal_ssrnat2coqnat; simpl;
omega.