- removed: cut_tac False to demostrate False

- removed: apply_tac Rle_zero_zero
- a new big example

diff --git a/helm/gTopLevel/esempi/fourier.cic b/helm/gTopLevel/esempi/fourier.cic
index dc883e4e4888fd11463339122b528af7320bd3d7..ba51e64ad80b3a8ee7dab716b0b34e6b93fe4f3f 100644 (file)
--- a/helm/gTopLevel/esempi/fourier.cic
+++ b/helm/gTopLevel/esempi/fourier.cic
@@ -12,7 +12,37 @@ alias R0        /Coq/Reals/Rdefinitions/R0.con
 alias R        /Coq/Reals/Rdefinitions/R.con
 alias eqT      /Coq/Init/Logic_Type/eqT.ind#1/1
 alias not      /Coq/Init/Logic/not.con
-
+alias or /Coq/Init/Logic/or.ind#1/1
+
+(*test real*)
+!x:R.!y:R.!z:R.
+(Rge
+(Rplus
+ (Rmult (Ropp (Rplus R1 R1)) x) (Rplus 
+   (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) y) (Rplus 
+     (Rmult (Rplus R1 (Rplus R1 R1)) z) R1)
+)) R0)
+->  
+(Rge
+(Rplus
+ (Rmult (Ropp (Rplus R1 (Rplus R1 R1))) x) (Rplus 
+   (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) y) (Rplus 
+      R1 (Rplus R1 R1))
+)) R0)
+->  
+(Rgt
+(Rplus
+  x (Rplus 
+   (Rmult (Rplus R1 R1) y) (Ropp z) )
+) R0)
+-> 
+(Rgt
+(Rplus
+ (Rmult (Rplus R1 (Rplus R1 R1)) x) (Rplus 
+   z (Ropp R1))
+) R0)
+
+-> (Rlt z R1)
 
 //test base1 ok
 !x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1))
@@ -25,19 +55,35 @@ alias not      /Coq/Init/Logic/not.con
 
 /Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con
 
+intros
+
 /Coq/Init/Logic/False.ind#1/1
 
-(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)))
+(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))))
 
 /Coq/fourier/Fourier_util/Rnot_le_le.con
 
 t1=(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y))
+
 t2=(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x))
+
+(t1-t2)=(Rminus 
+(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)))
+
 tc=(Rmult (Ropp R1) (Rinv R1))
 
 rewrite=(eqT R (Rminus (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x))
  (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y))) (Rmult (Ropp R1) (Rinv R1)))
 
+change=(not (or 
+(Rlt R0 (Rmult (Ropp R1) (Rinv R1))) 
+(eqT R R0 (Rmult (Ropp R1) (Rinv R1))) 
+))
+
+tac2
+/Coq/fourier/Fourier_util/Rnot_lt0.con
+
 //test base4 ok
 !x:R.!y:R.(Rgt x y) -> (Rle (Rminus y R1) (Rplus x R1))
 

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 90657b598fbbcaf5576e32e4b423489c143f56a3..17ff3f8fe732a37a923a6a3b2a91346ba7f98ccc 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -531,8 +531,8 @@ let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string
  "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") [] ;;
 let _Rle_zero_pos_plus1 =  Cic.Const (UriManager.uri_of_string 
  "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") [] ;;
-let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string 
- "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") [] ;;
+(*let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") [] ;;*)
 let _Rlt = Cic.Const (UriManager.uri_of_string 
  "cic:/Coq/Reals/Rdefinitions/Rlt.con") [] ;;
 let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string 
@@ -647,11 +647,11 @@ let tac_zero_infeq_pos gl (n,d) ~status =
  (*let cste = pf_parse_constr gl in*)
  debug("inizio tac_zero_infeq_pos\n");
  let tacn = ref 
-  (if n=0 then
+  (*(if n=0 then
     (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero ) 
-   else
+   else*)
     (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 )
-  )
+ (* ) *)
   in
   let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
   for i=1 to n-1 do 
@@ -748,8 +748,10 @@ let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) =
   let metasenv' = (fresh_meta,context,t)::metasenv in
    let proof' = curi,metasenv',pbo,pty in
     let proof'',goals =
-     PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast (Cic.Meta 
-      (fresh_meta,irl),t))::al)) ~status:(proof',goal)
+     PrimitiveTactics.apply_tac 
+      (*~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) (* ??? *)*)
+      ~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al)) (* ??? *)
+       ~status:(proof',goal)
     in
      proof'',fresh_meta::goals
 ;;
@@ -1141,7 +1143,7 @@ theoreme,so let's parse our thesis *)
        in
        tac:=(Tacticals.thens 
          ~start:(my_cut ~term:ineq) 
-         ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)Tacticals.then_  
+         ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)(**)Tacticals.then_  
           ~start:(fun ~status:(proof,goal as status) ->
              let curi,metasenv,pbo,pty = proof in
              let metano,context,ty = List.find (function (m,_,_) -> m=goal) 
@@ -1170,25 +1172,6 @@ theoreme,so let's parse our thesis *)
                   r)
                 ~continuations:
                    [PrimitiveTactics.apply_tac ~term:_Rinv_R1
-(* CSC: Il nostro goal e' 1^-1 = 1 e non 1 = 1^-1. Quindi non c'e' bisogno
-   di applicare sym_eqT. Perche' in Coq il goal e' al contrario? Forse i
-   parametri della equality_replace vengono passati al contrario? Oppure la
-   tattica usa i parametri al contrario?
-   CODICE NEL COMMENTO NON PORTATO. ORA ESISTE ANCHE LA TATTICA symmetry_tac
-                ~continuations:[Tacticals.then_ 
-                  ~start:(
-                    fun ~status:(proof,goal as status) ->
-                    debug("ECCOCI\n");
-                     let curi,metasenv,pbo,pty = proof in
-                    let metano,context,ty = List.find (function (m,_,_) -> m=
-                     goal) metasenv in
-                     debug("ty = "^CicPp.ppterm ty^"\n");
-                    let r = PrimitiveTactics.apply_tac ~term:_sym_eqT 
-                     ~status in
-                    debug("fine ECCOCI\n");
-                    r)
-                  ~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1)
-*)
                 ;Tacticals.try_tactics 
                   ~tactics:[ "ring", (fun ~status -> 
                                        debug("begin RING\n");
@@ -1197,7 +1180,8 @@ theoreme,so let's parse our thesis *)
                                        r)
                        ; "id", Tacticals.id_tac] 
                 ])
-              ;Tacticals.then_ 
+              ;(*Tacticals.id_tac*)
+               Tacticals.then_ 
                 ~start:
                  (
                  fun ~status:(proof,goal as status) ->
@@ -1215,6 +1199,7 @@ theoreme,so let's parse our thesis *)
                   let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 ~status in
                   debug("fine MY_CHNGE\n");
                   r
+                  
                  ) 
                 ~continuation:(*PORTINGTacticals.id_tac*)tac2]))
         ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*)
@@ -1223,14 +1208,18 @@ theoreme,so let's parse our thesis *)
         ~continuations:[Tacticals.then_ 
           ~start:(PrimitiveTactics.intros_tac ~name:"??")
           ~continuation:contradiction_tac
-        ;!tac])*)
-        tac:=!tac
+        ;!tac]) FIXED - this was useless*)
+       (* tac:=!tac*)
 
 
     |_-> assert false)(*match (!lutil) *)
   |_-> assert false); (*match res*)
   debug ("finalmente applico tac\n");
-  (!tac ~status:(proof,goal)) 
+  (
+  let r = !tac ~status:(proof,goal) in
+  debug("\n\n]]]]]]]]]]]]]]]]]) That's all folks ([[[[[[[[[[[[[[[[[[[\n\n");r
+  
+  ) 
 ;;
 
 let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;