From a2f9236b189b39bb5e7d864991cae29c9f9cb67f Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 7 Mar 2007 11:29:03 +0000 Subject: [PATCH] Relational: one file was missing :-) Procedural: the cic object preprocessor was not added to svn :-) --- .../acic_procedural/proceduralPreprocess.ml | 177 ++++++++++++++++++ .../acic_procedural/proceduralPreprocess.mli | 28 +++ matita/contribs/RELATIONAL/NLE/order.ma | 56 ++++++ 3 files changed, 261 insertions(+) create mode 100644 components/acic_procedural/proceduralPreprocess.ml create mode 100644 components/acic_procedural/proceduralPreprocess.mli create mode 100644 matita/contribs/RELATIONAL/NLE/order.ma diff --git a/components/acic_procedural/proceduralPreprocess.ml b/components/acic_procedural/proceduralPreprocess.ml new file mode 100644 index 000000000..d31d0113b --- /dev/null +++ b/components/acic_procedural/proceduralPreprocess.ml @@ -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/components/acic_procedural/proceduralPreprocess.mli b/components/acic_procedural/proceduralPreprocess.mli new file mode 100644 index 000000000..7bd55f4e2 --- /dev/null +++ b/components/acic_procedural/proceduralPreprocess.mli @@ -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/matita/contribs/RELATIONAL/NLE/order.ma b/matita/contribs/RELATIONAL/NLE/order.ma new file mode 100644 index 000000000..71de65d1d --- /dev/null +++ b/matita/contribs/RELATIONAL/NLE/order.ma @@ -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. -- 2.39.2