From 56e23ea031f695e40879053ff09e97ecec2507e1 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 28 Oct 2013 19:37:36 +0000 Subject: [PATCH] lazy equivalence for local environments is now defined its reflexivity reveals a bug in ldrop :( --- .../lambdadelta/basic_2/computation/fleq.ma | 4 ++-- .../basic_2/notation/relations/lazyeq_3.ma | 19 +++++++++++++++++++ .../basic_2/notation/relations/lazyeq_6.ma | 19 +++++++++++++++++++ .../relations/{fleq_8.ma => lazyeq_8.ma} | 2 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 6 +++++- 5 files changed, 46 insertions(+), 4 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_3.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_6.ma rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{fleq_8.ma => lazyeq_8.ma} (96%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fleq.ma index 2448b5260..da608196c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fleq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/fleq_8.ma". +include "basic_2/notation/relations/lazyeq_8.ma". include "basic_2/computation/lpxs.ma". (* EQUIVALENT "BIG TREE" NORMAL FORMS ***************************************) @@ -24,7 +24,7 @@ definition fleq: ∀h. sd h → tri_relation genv lenv term ≝ interpretation "equivalent 'big tree' normal forms (closure)" - 'FLEq h g G1 L1 T1 G2 L2 T2 = (fleq h g G1 L1 T1 G2 L2 T2). + 'LazyEq h g G1 L1 T1 G2 L2 T2 = (fleq h g G1 L1 T1 G2 L2 T2). (* Basic_properties *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_3.ma new file mode 100644 index 000000000..acae727a4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_3.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( L1 ⋕ break [ term 46 T ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'LazyEq $T $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_6.ma new file mode 100644 index 000000000..105a47363 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_6.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⋕ break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'LazyEq $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/fleq_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_8.ma similarity index 96% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/fleq_8.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_8.ma index 4e30eb6fc..052b1ad75 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/fleq_8.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_8.ma @@ -16,4 +16,4 @@ notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⋕ break [ term 46 h , break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" non associative with precedence 45 - for @{ 'FLEq $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. + for @{ 'LazyEq $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index d91e8d629..036726dcc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -236,7 +236,11 @@ table { [ { "lazy equivalence for closures" * } { [ "fleq ( ⦃?,?,?⦄ ⋕ ⦃?,?,?⦄ )" "fleq_fleq" * ] } - ] + ] + [ { "lazy equivalence for local environments" * } { + [ "lleq ( ? ⋕[?] ? )" "lleq_fleq" * ] + } + ] [ { "global env. slicing" * } { [ "gdrop ( ⇩[?] ? ≡ ? )" "gdrop_gdrop" * ] } -- 2.39.2