helm/gTopLevel/esempi/fourier/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 Rmult    /Coq/Reals/Rdefinitions/Rmult.con
  10 alias R1        /Coq/Reals/Rdefinitions/R1.con
  11 alias R0        /Coq/Reals/Rdefinitions/R0.con
  12 alias R        /Coq/Reals/Rdefinitions/R.con
  13 alias eqT       /Coq/Init/Logic_Type/eqT.ind#1/1
  14 alias not      /Coq/Init/Logic/not.con
  15 alias or /Coq/Init/Logic/or.ind#1/1
  16
  17 !x:R.
  18 (Rlt (Rmult(Ropp x)R1)
  19 R0)
  20 ->(Rlt R0 x)
  21
  22 // test 3x4 -> 35''
  23 !x:R.!y:R.!z:R.
  24 (Rge
  25 (Rplus
  26  (Rmult (Ropp (Rplus R1 R1)) x) (Rplus
  27    (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) y) (Rplus
  28      (Rmult (Rplus R1 (Rplus R1 R1)) z) R1)
  29 )) R0)
  30 ->
  31 (Rge
  32 (Rplus
  33  (Rmult (Ropp (Rplus R1 (Rplus R1 R1))) x) (Rplus
  34    (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) y) (Rplus
  35       R1 (Rplus R1 R1))
  36 )) R0)
  37 ->
  38 (Rgt
  39 (Rplus
  40   x (Rplus
  41    (Rmult (Rplus R1 R1) y) (Ropp z) )
  42 ) R0)
  43 ->
  44 (Rgt
  45 (Rplus
  46  (Rmult (Rplus R1 (Rplus R1 R1)) x) (Rplus
  47    z (Ropp R1))
  48 ) R0)
  49
  50 -> (Rlt z R1)
  51
  52 // test 6x6 ->
  53
  54 !x:R.!y:R.!z:R.!t:R.!u:R.!v:R.
  55 (Rgt
  56 (Rplus (Ropp x) (Rplus y (Rplus z (Rplus t (Rplus u (Rplus v (Rplus R1 R1)))))))
  57   R0)
  58 ->
  59 (Rgt
  60 (Rplus x (Rplus (Ropp y) (Rplus (Ropp z) (Rplus (Ropp t) (Rplus (Ropp u) (Rplus R1 R1))))))
  61   R0)
  62 ->
  63 (Rgt
  64 (Rplus y (Rplus (Ropp z) (Rplus t (Rplus u (Rplus R1 R1)))))
  65   R0)
  66 ->
  67 (Rgt
  68 (Rplus y (Rplus z (Rplus (Ropp t) (Rplus (Ropp (Rmult (Rplus R1 R1)v)) (Rplus R1 R1)))))
  69   R0)
  70 ->
  71 (Rgt
  72 (Rplus y (Rplus z (Rplus t (Rplus (Ropp u) (Rplus R1 R1)))))
  73   R0)
  74 ->
  75 (Rlt
  76 (Rplus (Rmult (Rplus R1 R1) x) (Rplus v y))
  77   R0)
  78 -> (Rlt (Rmult (Rplus R1 R1) x) R0)
  79
  80
  81
  82
  83
  84
  85 //test base1 ok
  86 !x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1))
  87
  88 //test base2 ok
  89 !x:R.!y:R.(Rlt x y) -> (Rgt (Rplus y R1) (Rminus x R1))
  90
  91 //test base3 ok
  92 !x:R.!y:R.(Rge x y) -> (Rlt (Rplus y R1) (Rplus x (Rplus R1 R1)))
  93
  94 /Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con
  95
  96 intros
  97
  98 /Coq/Init/Logic/False.ind#1/1
  99
 100 (not (Rle (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y)) (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x))))
 101
 102 /Coq/fourier/Fourier_util/Rnot_le_le.con
 103
 104 t1=(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y))
 105
 106 t2=(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x))
 107
 108 (t1-t2)=(Rminus
 109 (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y))
 110 (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x)))
 111
 112 tc=(Rmult (Ropp R1) (Rinv R1))
 113
 114 rewrite=(eqT R (Rminus (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x))
 115  (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y))) (Rmult (Ropp R1) (Rinv R1)))
 116
 117 change=(not (or
 118 (Rlt R0 (Rmult (Ropp R1) (Rinv R1)))
 119 (eqT R R0 (Rmult (Ropp R1) (Rinv R1)))
 120 ))
 121
 122 tac2
 123 /Coq/fourier/Fourier_util/Rnot_lt0.con
 124
 125 //test base4 ok
 126 !x:R.!y:R.(Rgt x y) -> (Rle (Rminus y R1) (Rplus x R1))
 127
 128 //test base5 ok
 129 !x:R.!y:R.(Rlt x ( Rplus y R1 ) ) -> (Rge (Rplus y (Rplus R1 R1)) (Rminus x R0))
 130
 131 //test base6 ok
 132 !x:R.!y:R.(eqT R x y) -> (Rgt (Rplus y R1) (Rminus x R1))
 133
 134 //test base7 (should fail) ok
 135 !x:R.!y:R.(Rlt x y) -> (Rlt (Rplus y R1) (Rminus x R1))
 136
 137