From 4e4c541d10848af70ef5cb2ff53e58c02cf8833f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 4 Nov 2002 12:00:33 +0000 Subject: [PATCH] - synchronization with the main branch --- helm/gTopLevel/esempi/fourier.cic | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/helm/gTopLevel/esempi/fourier.cic b/helm/gTopLevel/esempi/fourier.cic index cae3925a7..09caea79b 100644 --- a/helm/gTopLevel/esempi/fourier.cic +++ b/helm/gTopLevel/esempi/fourier.cic @@ -1,8 +1,35 @@ alias Rge /Coq/Reals/Rdefinitions/Rge.con alias Rle /Coq/Reals/Rdefinitions/Rle.con +alias Rgt /Coq/Reals/Rdefinitions/Rgt.con +alias Rlt /Coq/Reals/Rdefinitions/Rlt.con +alias Ropp /Coq/Reals/Rdefinitions/Ropp.con +alias Rinv /Coq/Reals/Rdefinitions/Rinv.con alias Rplus /Coq/Reals/Rdefinitions/Rplus.con alias Rminus /Coq/Reals/Rdefinitions/Rminus.con alias R1 /Coq/Reals/Rdefinitions/R1.con +alias R0 /Coq/Reals/Rdefinitions/R0.con alias R /Coq/Reals/Rdefinitions/R.con +alias Eq /Coq/Init/Logic_Type/eqT.ind#1/1 +//test base1 ok !x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1)) + +//test base2 ok +!x:R.!y:R.(Rlt x y) -> (Rgt (Rplus y R1) (Rminus x R1)) + +//test base3 (unification fails) +!x:R.!y:R.(Rge x y) -> (Rlt (Rplus y R1) (Rplus x (Rplus R1 R1))) + +//test base4 ok +!x:R.!y:R.(Rgt x y) -> (Rle (Rminus y R1) (Rplus x R1)) + +//test base5 ok +!x:R.!y:R.(Rlt x ( Rplus y R1 ) ) -> (Rge (Rplus y (Rplus R1 R1)) (Rminus x R0)) + +//test base6 (unification fails) +!x:R.!y:R.(Eq R x y) -> (Rgt (Rplus y R1) (Rminus x R1)) + +//test base7 (should fail) ok +!x:R.!y:R.(Rlt x y) -> (Rlt (Rplus y R1) (Rminus x R1)) + + -- 2.39.2