]> matita.cs.unibo.it Git - helm.git/commitdiff
Relational: one file was missing :-)
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 7 Mar 2007 11:29:03 +0000 (11:29 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 7 Mar 2007 11:29:03 +0000 (11:29 +0000)
Procedural: the cic object preprocessor was not added to svn :-)

helm/software/components/acic_procedural/proceduralPreprocess.ml [new file with mode: 0644]
helm/software/components/acic_procedural/proceduralPreprocess.mli [new file with mode: 0644]
helm/software/matita/contribs/RELATIONAL/NLE/order.ma [new file with mode: 0644]

diff --git a/helm/software/components/acic_procedural/proceduralPreprocess.ml b/helm/software/components/acic_procedural/proceduralPreprocess.ml
new file mode 100644 (file)
index 0000000..d31d011
--- /dev/null
@@ -0,0 +1,177 @@
+(* Copyright (C) 2003-2005, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+module C    = Cic
+module Un   = CicUniv
+module S    = CicSubstitution
+module R    = CicReduction
+module TC   = CicTypeChecker 
+module DTI  = DoubleTypeInference
+module HEL  = HExtlib
+
+(* helper functions *********************************************************)
+
+let identity x = x
+
+let comp f g x = f (g x)
+
+let get_type c t =
+   let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty
+
+let is_proof c t =
+   match (get_type c (get_type c t)) with
+      | C.Sort C.Prop -> true
+      | _             -> false
+
+let is_not_atomic = function
+   | C.Sort _
+   | C.Rel _
+   | C.Const _
+   | C.Var _
+   | C.MutInd _ 
+   | C.MutConstruct _ -> false
+   | _                -> true
+
+let split c t =
+   let add s v c = Some (s, C.Decl v) :: c in
+   let rec aux whd a n c = function
+      | C.Prod (s, v, t)  -> aux false (v :: a) (succ n) (add s v c) t
+      | v when whd        -> v :: a, n
+      | v                 -> aux true a n c (R.whd ~delta:true c v)
+    in
+    aux false [] 0 c t
+
+let add g htbl t proof decurry =
+   if proof then C.CicHash.add htbl t decurry; 
+   g t proof decurry
+
+let find g htbl t = 
+   try 
+      let decurry = C.CicHash.find htbl t in g t true decurry
+   with Not_found -> g t false 0
+
+(* term preprocessing *******************************************************)
+
+let expanded_premise = "EXPANDED"
+
+let defined_premise = "DEFINED"
+
+let eta_expand n t =
+   let ty = C.Implicit None in
+   let name i = Printf.sprintf "%s%u" expanded_premise i in 
+   let lambda i t = C.Lambda (C.Name (name i), ty, t) in
+   let arg i n = C.Rel (n - i) in
+   let rec aux i f a =
+      if i >= n then f, a else aux (succ i) (comp f (lambda i)) (arg i n :: a)
+   in
+   let absts, args = aux 0 identity [] in
+   absts (C.Appl (S.lift n t :: args))
+
+let eta_fix t proof decurry =
+   if proof && decurry > 0 then eta_expand decurry t else t
+
+let rec pp_cast g ht es c t v =
+   if es then pp_proof g ht es c t else find g ht t
+
+and pp_lambda g ht es c name v t =
+   let name = if DTI.does_not_occur 1 t then C.Anonymous else name in
+   let entry = Some (name, C.Decl v) in
+   let g t _ decurry = 
+      let t = eta_fix t true decurry in
+      g (C.Lambda (name, v, t)) true 0 in
+   if es then pp_proof g ht es (entry :: c) t else find g ht t
+
+and pp_letin g ht es c name v t =
+   let entry = Some (name, C.Def (v, None)) in
+   let g t _ decurry =
+      if DTI.does_not_occur 1 t then g (S.lift (-1) t) true decurry else 
+      let g v proof d = match v with
+         | C.LetIn (mame, w, u) when proof ->
+            let x = C.LetIn (mame, w, C.LetIn (name, u, S.lift_from 2 1 t)) in
+           pp_proof g ht false c x 
+         | v                               -> 
+            let v = eta_fix v proof d in
+           g (C.LetIn (name, v, t)) true decurry
+      in
+      if es then pp_term g ht es c v else find g ht v
+   in
+   if es then pp_proof g ht es (entry :: c) t else find g ht t
+
+and pp_appl_one g ht es c t v =
+   let g t _ decurry =
+      let g v proof d =
+         match t, v with
+           | t, C.LetIn (mame, w, u) when proof ->
+               let x = C.LetIn (mame, w, C.Appl [S.lift 1 t; u]) in
+              pp_proof g ht false c x 
+            | C.LetIn (mame, w, u), v            ->
+               let x = C.LetIn (mame, w, C.Appl [u; S.lift 1 v]) in
+              pp_proof g ht false c x
+           | C.Appl ts, v when decurry > 0      ->
+              let v = eta_fix v proof d in
+              g (C.Appl (List.append ts [v])) true (pred decurry)
+           | t, v  when is_not_atomic t         ->
+              let mame = C.Name defined_premise in
+              let x = C.LetIn (mame, t, C.Appl [C.Rel 1; S.lift 1 v]) in
+              pp_proof g ht false c x
+           | t, v                               ->
+               let _, premsno = split c (get_type c t) in
+              let v = eta_fix v proof d in
+               g (C.Appl [t; v]) true (pred premsno)
+      in
+      if es then pp_term g ht es c v else find g ht v
+   in
+   if es then pp_proof g ht es c t else find g ht t
+
+and pp_appl g ht es c t = function
+   | []             -> pp_proof g ht es c t
+   | [v]            -> pp_appl_one g ht es c t v
+   | v1 :: v2 :: vs ->
+      let x = C.Appl (C.Appl [t; v1] :: v2 :: vs) in 
+      pp_proof g ht es c x
+
+and pp_proof g ht es c t = 
+   let g t proof decurry = add g ht t proof decurry in
+   match t with
+      | C.Cast (t, v)         -> pp_cast g ht es c t v
+      | C.Lambda (name, v, t) -> pp_lambda g ht es c name v t
+      | C.LetIn (name, v, t)  -> pp_letin g ht es c name v t
+      | C.Appl (t :: vs)      -> pp_appl g ht es c t vs
+      | t                     -> g t true 0
+
+and pp_term g ht es c t =
+   if is_proof c t then pp_proof g ht es c t else g t false 0
+
+(* object preprocessing *****************************************************)
+
+let pp_obj = function
+   | C.Constant (name, Some bo, ty, pars, attrs) ->
+      let g bo proof decurry = 
+         let bo = eta_fix bo proof decurry in
+         C.Constant (name, Some bo, ty, pars, attrs)
+      in
+      let ht = C.CicHash.create 1 in
+      pp_term g ht true [] bo
+   | obj                                         -> obj
diff --git a/helm/software/components/acic_procedural/proceduralPreprocess.mli b/helm/software/components/acic_procedural/proceduralPreprocess.mli
new file mode 100644 (file)
index 0000000..7bd55f4
--- /dev/null
@@ -0,0 +1,28 @@
+(* Copyright (C) 2003-2005, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+val split: Cic.context -> Cic.term -> Cic.term list * int
+
+val pp_obj: Cic.obj -> Cic.obj
diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/order.ma b/helm/software/matita/contribs/RELATIONAL/NLE/order.ma
new file mode 100644 (file)
index 0000000..71de65d
--- /dev/null
@@ -0,0 +1,56 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/RELATIONAL/NLE/order".
+
+include "NLE/inv.ma".
+
+theorem nle_refl: \forall x. x <= x.
+ intros; elim x; clear x; auto.
+qed.
+
+theorem nle_trans: \forall x,y. x <= y \to
+                   \forall z. y <= z \to x <= z.
+ intros 3. elim H; clear H x y;
+ [ auto
+ | lapply linear nle_inv_succ_1 to H3. decompose. subst. 
+   auto
+ ].
+qed.
+
+theorem nle_false: \forall x,y. x <= y \to y < x \to False.
+ intros 3; elim H; clear H x y; auto.
+qed.
+
+theorem nle_irrefl: \forall x. x < x \to False.
+ intros. auto.
+qed.
+
+theorem nle_irrefl_ei: \forall x, z. z <= x \to z = succ x \to False.
+ intros 3. elim H; clear H x z;
+ [ destruct H1
+ | destruct H3. clear H3. subst. auto.
+ ].
+qed.
+
+theorem nle_irrefl_smart: \forall x. x < x \to False.
+ intros 1. elim x; clear x; auto.
+qed.
+
+theorem nle_lt_or_eq: \forall y, x. x <= y \to x < y \lor x = y.
+ intros. elim H; clear H x y;
+ [ elim n; clear n
+ | decompose
+ ]; auto.
+qed.