From f8bc120b39bd74ade4e11d4d3ef4355f66c42495 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 23 Nov 2012 22:19:23 +0000
Subject: [PATCH] additions in lift.ma ....

---
 matita/matita/contribs/lambda/lift.ma         | 16 ++++++-
 matita/matita/contribs/lambda/preamble.ma     | 37 ++++++++++++++++
 matita/matita/contribs/lambda/term.ma         |  2 +-
 matita/matita/contribs/lambda/trichotomy.ma   | 42 -------------------
 matita/matita/contribs/lambda/xoa.conf.xml    |  1 +
 matita/matita/contribs/lambda/xoa.ma          | 10 +++++
 matita/matita/contribs/lambda/xoa_notation.ma |  6 +++
 7 files changed, 70 insertions(+), 44 deletions(-)
 delete mode 100644 matita/matita/contribs/lambda/trichotomy.ma

diff --git a/matita/matita/contribs/lambda/lift.ma b/matita/matita/contribs/lambda/lift.ma
index 4383713e7..6a9b8d510 100644
--- a/matita/matita/contribs/lambda/lift.ma
+++ b/matita/matita/contribs/lambda/lift.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "trichotomy.ma".
 include "term.ma".
 
 (* RELOCATION ***************************************************************)
@@ -50,6 +49,21 @@ lemma lift_vref_ge: ∀d,h,i. d ≤ i → ↑[d, h] #i = #(i+h).
 normalize // /3 width=1/
 qed.
 
+lemma lift_inv_vref_lt: ∀j,d. j < d → ∀h,M. ↑[d, h] M = #j → M = #j.
+#j #d #Hjd #h * normalize
+[ #i elim (lt_or_eq_or_gt i d) #Hid
+  [ >(tri_lt ???? … Hid) -Hid -Hjd //
+  | #H destruct >tri_eq in Hjd; #H
+    elim (plus_lt_false … H)
+  | >(tri_gt ???? … Hid)
+    lapply (transitive_lt … Hjd Hid) -Hjd -Hid #H #H0 destruct
+    elim (plus_lt_false … H)
+  ]
+| #A #H destruct
+| #B #A #H destruct
+]
+qed.
+
 lemma lift_inv_abst: ∀C,d,h,M. ↑[d, h] M = 𝛌.C →
                      ∃∃A. ↑[d+1, h] A = C & M = 𝛌.A.
 #C #d #h * normalize
diff --git a/matita/matita/contribs/lambda/preamble.ma b/matita/matita/contribs/lambda/preamble.ma
index 53a433d40..afaacb5f2 100644
--- a/matita/matita/contribs/lambda/preamble.ma
+++ b/matita/matita/contribs/lambda/preamble.ma
@@ -31,3 +31,40 @@ qed-.
 lemma lt_zero_false: ∀n. n < 0 → ⊥.
 #n #H elim (lt_to_not_le … H) -H /2 width=1/
 qed-.
+
+lemma plus_lt_false: ∀m,n. m + n < m → ⊥.
+#m #n #H elim (lt_to_not_le … H) -H /2 width=1/
+qed-.
+
+lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m.
+#m #n elim (lt_or_ge m n) /2 width=1/
+#H elim H -m /2 width=1/
+#m #Hm * #H /2 width=1/ /3 width=1/
+qed-.
+
+(* trichotomy operator *)
+
+(* Note: this is "if eqb n1 n2 then a2 else if leb n1 n2 then a1 else a3" *)
+let rec tri (A:Type[0]) n1 n2 a1 a2 a3 on n1 : A ≝
+  match n1 with 
+  [ O    ⇒ match n2 with [ O ⇒ a2 | S n2 ⇒ a1 ]
+  | S n1 ⇒ match n2 with [ O ⇒ a3 | S n2 ⇒ tri A n1 n2 a1 a2 a3 ]
+  ].
+
+lemma tri_lt: ∀A,a1,a2,a3,n2,n1. n1 < n2 → tri A n1 n2 a1 a2 a3 = a1.
+#A #a1 #a2 #a3 #n2 elim n2 -n2
+[ #n1 #H elim (lt_zero_false … H)
+| #n2 #IH #n1 elim n1 -n1 // /3 width=1/
+]
+qed.
+
+lemma tri_eq: ∀A,a1,a2,a3,n. tri A n n a1 a2 a3 = a2.
+#A #a1 #a2 #a3 #n elim n -n normalize //
+qed.
+
+lemma tri_gt: ∀A,a1,a2,a3,n1,n2. n2 < n1 → tri A n1 n2 a1 a2 a3 = a3.
+#A #a1 #a2 #a3 #n1 elim n1 -n1
+[ #n2 #H elim (lt_zero_false … H)
+| #n1 #IH #n2 elim n2 -n2 // /3 width=1/
+]
+qed.
diff --git a/matita/matita/contribs/lambda/term.ma b/matita/matita/contribs/lambda/term.ma
index 7710c05fb..a38508ada 100644
--- a/matita/matita/contribs/lambda/term.ma
+++ b/matita/matita/contribs/lambda/term.ma
@@ -18,7 +18,7 @@ include "preamble.ma".
 
 (* TERM STRUCTURE ***********************************************************)
 
-(* Policy: term metavariables: A, B, C, D
+(* Policy: term metavariables: A, B, C, D, M, N
            de Bruijn indexes : i, j
 *)
 inductive term: Type[0] ≝
diff --git a/matita/matita/contribs/lambda/trichotomy.ma b/matita/matita/contribs/lambda/trichotomy.ma
deleted file mode 100644
index 52dc027d4..000000000
--- a/matita/matita/contribs/lambda/trichotomy.ma
+++ /dev/null
@@ -1,42 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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 "preamble.ma".
-
-(* TRICHOTOMY OPERATOR ******************************************************)
-
-(* Note: this is "if eqb n1 n2 then a2 else if leb n1 n2 then a1 else a3" *)
-let rec tri (A:Type[0]) n1 n2 a1 a2 a3 on n1 : A ≝
-  match n1 with 
-  [ O    ⇒ match n2 with [ O ⇒ a2 | S n2 ⇒ a1 ]
-  | S n1 ⇒ match n2 with [ O ⇒ a3 | S n2 ⇒ tri A n1 n2 a1 a2 a3 ]
-  ].
-
-lemma tri_lt: ∀A,a1,a2,a3,n2,n1. n1 < n2 → tri A n1 n2 a1 a2 a3 = a1.
-#A #a1 #a2 #a3 #n2 elim n2 -n2
-[ #n1 #H elim (lt_zero_false … H)
-| #n2 #IH #n1 elim n1 -n1 // /3 width=1/
-]
-qed.
-
-lemma tri_eq: ∀A,a1,a2,a3,n. tri A n n a1 a2 a3 = a2.
-#A #a1 #a2 #a3 #n elim n -n normalize //
-qed.
-
-lemma tri_gt: ∀A,a1,a2,a3,n1,n2. n2 < n1 → tri A n1 n2 a1 a2 a3 = a3.
-#A #a1 #a2 #a3 #n1 elim n1 -n1
-[ #n2 #H elim (lt_zero_false … H)
-| #n1 #IH #n2 elim n2 -n2 // /3 width=1/
-]
-qed.
diff --git a/matita/matita/contribs/lambda/xoa.conf.xml b/matita/matita/contribs/lambda/xoa.conf.xml
index 72b1258bd..620113e79 100644
--- a/matita/matita/contribs/lambda/xoa.conf.xml
+++ b/matita/matita/contribs/lambda/xoa.conf.xml
@@ -10,5 +10,6 @@
     <key name="include">basics/pts.ma</key>
     <key name="ex">2 1</key>
     <key name="ex">3 2</key>
+    <key name="or">3</key>
   </section>
 </helm_registry>
diff --git a/matita/matita/contribs/lambda/xoa.ma b/matita/matita/contribs/lambda/xoa.ma
index 4e6e6aed9..1a92dbad0 100644
--- a/matita/matita/contribs/lambda/xoa.ma
+++ b/matita/matita/contribs/lambda/xoa.ma
@@ -32,3 +32,13 @@ inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0→A1→Prop) : Prop ≝
 
 interpretation "multiple existental quantifier (3, 2)" 'Ex P0 P1 P2 = (ex3_2 ? ? P0 P1 P2).
 
+(* multiple disjunction connective (3) *)
+
+inductive or3 (P0,P1,P2:Prop) : Prop ≝
+   | or3_intro0: P0 → or3 ? ? ?
+   | or3_intro1: P1 → or3 ? ? ?
+   | or3_intro2: P2 → or3 ? ? ?
+.
+
+interpretation "multiple disjunction connective (3)" 'Or P0 P1 P2 = (or3 P0 P1 P2).
+
diff --git a/matita/matita/contribs/lambda/xoa_notation.ma b/matita/matita/contribs/lambda/xoa_notation.ma
index b6498bb76..a2a26eb6e 100644
--- a/matita/matita/contribs/lambda/xoa_notation.ma
+++ b/matita/matita/contribs/lambda/xoa_notation.ma
@@ -34,3 +34,9 @@ notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19
  non associative with precedence 20
  for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) }.
 
+(* multiple disjunction connective (3) *)
+
+notation "hvbox(∨∨ term 29 P0 break | term 29 P1 break | term 29 P2)"
+ non associative with precedence 30
+ for @{ 'Or $P0 $P1 $P2 }.
+
-- 
2.39.2