]> matita.cs.unibo.it Git - helm.git/blob - helm/gTopLevel/esempi/fourier.cic
snapshot
[helm.git] / helm / gTopLevel / esempi / fourier.cic
1 alias Rge       /Coq/Reals/Rdefinitions/Rge.con
2 alias Rle       /Coq/Reals/Rdefinitions/Rle.con
3 alias Rgt       /Coq/Reals/Rdefinitions/Rgt.con
4 alias Rlt       /Coq/Reals/Rdefinitions/Rlt.con
5 alias Ropp     /Coq/Reals/Rdefinitions/Ropp.con
6 alias Rinv     /Coq/Reals/Rdefinitions/Rinv.con
7 alias Rplus     /Coq/Reals/Rdefinitions/Rplus.con
8 alias Rminus    /Coq/Reals/Rdefinitions/Rminus.con
9 alias R1        /Coq/Reals/Rdefinitions/R1.con
10 alias R0        /Coq/Reals/Rdefinitions/R0.con
11 alias R        /Coq/Reals/Rdefinitions/R.con
12 alias Eq        /Coq/Init/Logic_Type/eqT.ind#1/1
13
14 //test base1 ok
15 !x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1))
16
17 //test base2 ok
18 !x:R.!y:R.(Rlt x y) -> (Rgt (Rplus y R1) (Rminus x R1))
19
20 //test base3 (unification fails)
21 !x:R.!y:R.(Rge x y) -> (Rlt (Rplus y R1) (Rplus x (Rplus R1 R1)))
22
23 //test base4 ok
24 !x:R.!y:R.(Rgt x y) -> (Rle (Rminus y R1) (Rplus x R1))
25
26 //test base5 ok
27 !x:R.!y:R.(Rlt x ( Rplus y R1 ) ) -> (Rge (Rplus y (Rplus R1 R1)) (Rminus x R0))
28
29 //test base6 (unification fails)
30 !x:R.!y:R.(Eq R x y) -> (Rgt (Rplus y R1) (Rminus x R1))
31
32 //test base7 (should fail) ok
33 !x:R.!y:R.(Rlt x y) -> (Rlt (Rplus y R1) (Rminus x R1))
34
35