--- /dev/null
+(* 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
--- /dev/null
+(* 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
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
projects / helm.git / commitdiff