From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 4 Jul 2014 18:08:34 +0000 (+0000)
Subject: conjecture on antisymmetry of cpr finally closed
X-Git-Tag: make_still_working~886
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=127be10fa95b5b347887241e046d72e432944e61;p=helm.git

conjecture on antisymmetry of cpr finally closed
cpr is NOT antisymmetric: call-by-value beta-reduction takes two steps exactly
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma b/matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma
new file mode 100644
index 000000000..84713bce6
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/reduction/cpr.ma".
+
+(* EXAMPLES *****************************************************************)
+
+(* A reduction cycle in two steps: the term Omega ***************************)
+
+definition Delta: term ≝ +ⓛ⋆0.ⓐ#0.#0.
+
+definition Omega1: term ≝ ⓐDelta.Delta.
+
+definition Omega2: term ≝ +ⓓⓝ⋆0.Delta.ⓐ#0.#0.
+
+(* Basic properties *********************************************************)
+
+lemma Delta_lift: ∀d,e. ⇧[d, e] Delta ≡ Delta.
+/4 width=1 by lift_flat, lift_bind, lift_lref_lt/ qed.
+
+(* Main properties **********************************************************)
+
+theorem cpr_Omega_12: ⦃⋆, ⋆⦄ ⊢ Omega1 ➡ Omega2.
+/2 width=1 by cpr_beta/ qed.
+
+theorem cpr_Omega_21: ⦃⋆, ⋆⦄ ⊢ Omega2 ➡ Omega1.
+@(cpr_zeta … Omega1) /2 width=1 by lift_flat/
+@cpr_flat @(cpr_delta … Delta ? 0)
+[3,5,8,10: // |4,9: /2 width=1 by cpr_eps/ |*: skip ]
+qed.
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 880a674aa..456a2b0e3 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
@@ -9,16 +9,23 @@ table {
         ]
      }
    ]
-(*
    class "wine"
    [ { "examples" * } {
         [ { "" * } {
-             [ "" * ]
+             [ "ex_cpr_omega" * ]
           }
         ]
      }
    ]
    class "magenta"
+   [ { "" * } {
+        [ { "" * } {
+             [ "" * ]
+          }
+        ]
+     }
+   ]
+(*   
    [ { "higher order dynamic typing" * } {
         [ { "higher order native type assignment" * } {
              [ "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ]