From 761967afe1bd46b21a6bd69232bf09e1658b0734 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 28 Nov 2008 21:41:19 +0000 Subject: [PATCH] cicDischarge: final fixup. Now correctly processes Coq/Init/Logic.mma :) We handle missing abstractions in MutCase output type procedural/Coq: we removed the depence from legacy --- .../cic_proof_checking/cicDischarge.ml | 43 +++++++++++++------ .../cic_proof_checking/cicDischarge.mli | 3 ++ .../matita/contribs/procedural/Coq/depends | 3 +- .../contribs/procedural/Coq/preamble.ma | 37 ++++++++++++---- .../matita/contribs/procedural/Coq/root | 1 - 5 files changed, 63 insertions(+), 24 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicDischarge.ml b/helm/software/components/cic_proof_checking/cicDischarge.ml index 4ad41eef7..65b5cea33 100644 --- a/helm/software/components/cic_proof_checking/cicDischarge.ml +++ b/helm/software/components/cic_proof_checking/cicDischarge.ml @@ -211,12 +211,20 @@ let rec discharge_term st t = match t with C.Lambda (C.Anonymous, vty, S.lift 1 wb) else (* Fixing needed, some right parametes *) - if frpsno = rpsno then - let vty, _ = TC.type_of_aux' [] st.c v' Un.default_ugraph in + if frpsno = rpsno && named then + let vty, _ = TC.type_of_aux' [] st.c v' Un.default_ugraph in if !debug then begin out "VTY: "; Ut.pp_term out [] st.c vty; out "\n" end; - let vty, wb = S.lift rpsno vty, S.lift (succ rpsno) wb in + let vty, wb = S.lift rpsno vty, S.lift 1 wb in + let vty = match vty with + | C.Appl (C.MutInd (fu, fm, _) as hd :: args) + when UM.eq fu u && fm = m && List.length args = psno -> + let largs, _ = X.split_nth lpsno args in + C.Appl (hd :: largs @ Ut.mk_rels rpsno 0) + | _ -> + assert false + in close false wc (C.Lambda (C.Anonymous, vty, wb)) (* This case should not happen *) else assert false @@ -294,14 +302,14 @@ let rec discharge_object dn du obj = if w' == w && vars = [] then obj else let w'' = sh w w' in (* We do not typecheck because variables are not closed *) - C.Variable (dn b, None, w'', [], attrs) + C.Variable (dn b, None, w'', vars, attrs) | C.Variable (b, Some v, w, vars, attrs) -> let st = init_status dn du ls vars in let w', v' = discharge_term st w, discharge_term st v in if w' == w && v' == v && vars = [] then obj else let w'', v'' = sh w w', sh v v' in (* We do not typecheck because variables are not closed *) - C.Variable (dn b, Some v'', w'', [], attrs) + C.Variable (dn b, Some v'', w'', vars, attrs) | C.Constant (b, None, w, vars, attrs) -> let st = init_status dn du ls vars in let w' = discharge_term st w in @@ -338,14 +346,23 @@ and discharge_uri dn du uri = obj', obj' == obj and discharge_vars dn du vars = -(* We should check that the dependences are ordered telesopically *) - let map u = - match discharge_uri dn du u with - | C.Variable (b, None, w, _, _), _ -> Some (C.Name b, C.Decl w) - | C.Variable (b, Some v, w, _, _), _ -> Some (C.Name b, C.Def (v, w)) - | _ -> None - in - List.rev_map map vars + let rec aux us c = function + | [] -> c + | u :: tl -> + let e = match discharge_uri dn du u with + | C.Variable (b, None, w, vars, _), _ -> + let map = relocate us (List.rev vars) in + let w = S.lift_map 1 map w in + Some (C.Name b, C.Decl w) + | C.Variable (b, Some v, w, vars, _), _ -> + let map = relocate us (List.rev vars) in + let v, w = S.lift_map 1 map v, S.lift_map 1 map w in + Some (C.Name b, C.Def (v, w)) + | _ -> assert false + in + aux (u :: us) (e :: c) tl + in + aux [] [] vars and init_status dn du ls vars = let c, rl = discharge_vars dn du vars, List.rev vars in diff --git a/helm/software/components/cic_proof_checking/cicDischarge.mli b/helm/software/components/cic_proof_checking/cicDischarge.mli index 7d6f630f4..2e2790a97 100644 --- a/helm/software/components/cic_proof_checking/cicDischarge.mli +++ b/helm/software/components/cic_proof_checking/cicDischarge.mli @@ -23,6 +23,9 @@ * http://cs.unibo.it/helm/. *) +(* NOTE. Discharged variables are not well formed. *) +(* For internal recursive use only. *) + (* discharges the explicit variables of the given object (with sharing) *) (* the first argument is a map for relacating the names of the objects *) (* the second argument is a map for relocating the uris of the dependencdes *) diff --git a/helm/software/matita/contribs/procedural/Coq/depends b/helm/software/matita/contribs/procedural/Coq/depends index 93dcd84fe..4bca3ab28 100644 --- a/helm/software/matita/contribs/procedural/Coq/depends +++ b/helm/software/matita/contribs/procedural/Coq/depends @@ -222,7 +222,7 @@ Reals/SplitRmult.mma Coq.ma Reals/Rbase.ma Sets/Relations_2.ma Sets/Relations_2.mma Reals/RList.ma Reals/RList.mma Arith/Max.mma Arith/Arith.ma Coq.ma -preamble.ma coq.ma +preamble.ma ZArith/Zorder.ma ZArith/Zorder.mma Sets/Image.ma Sets/Image.mma NArith/BinPos.ma NArith/BinPos.mma @@ -392,4 +392,3 @@ Wellfounded/Wellfounded.mma Coq.ma Wellfounded/Disjoint_Union.ma Wellfounded/Inc ZArith/Zcomplements.mma Arith/Wf_nat.ma Coq.ma Lists/List.ma ZArith/ZArith_base.ma Logic/Classical_Pred_Type.ma Logic/Classical_Pred_Type.mma Reals/Rtrigo_alt.mma Coq.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo_def.ma Reals/SeqSeries.ma -coq.ma diff --git a/helm/software/matita/contribs/procedural/Coq/preamble.ma b/helm/software/matita/contribs/procedural/Coq/preamble.ma index a5875f573..04d88dc07 100644 --- a/helm/software/matita/contribs/procedural/Coq/preamble.ma +++ b/helm/software/matita/contribs/procedural/Coq/preamble.ma @@ -12,11 +12,32 @@ (* *) (**************************************************************************) -include "coq.ma". -(* -alias id "refl_equal" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)". -alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)". -alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)". -alias id "I" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1/1)". -alias id "sym_eq" = "cic:/Coq/Init/Logic/sym_eq.con". -*) +default "equality" + cic:/Coq/Init/Logic/eq.ind + cic:/Coq/Init/Logic/sym_eq.con + cic:/Coq/Init/Logic/trans_eq.con + cic:/Coq/Init/Logic/eq_ind.con + cic:/Coq/Init/Logic/eq_ind_r.con + cic:/Coq/Init/Logic/eq_rec.con + cic:/Coq/Init/Logic/eq_rec_r.con + cic:/Coq/Init/Logic/eq_rect.con + cic:/Coq/Init/Logic/eq_rect_r.con + cic:/Coq/Init/Logic/f_equal.con + cic:/matita/procedural/Coq/preamble/f_equal1.con. + +default "true" + cic:/Coq/Init/Logic/True.ind. +default "false" + cic:/Coq/Init/Logic/False.ind. +default "absurd" + cic:/Coq/Init/Logic/absurd.con. + +interpretation "Coq's leibnitz's equality" 'eq x y = (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y). + +theorem f_equal1 : \forall A,B:Type.\forall f:A\to B.\forall x,y:A. + x = y \to (f y) = (f x). + intros. + symmetry. + apply cic:/Coq/Init/Logic/f_equal.con. + assumption. +qed. diff --git a/helm/software/matita/contribs/procedural/Coq/root b/helm/software/matita/contribs/procedural/Coq/root index 50d22b013..15286f493 100644 --- a/helm/software/matita/contribs/procedural/Coq/root +++ b/helm/software/matita/contribs/procedural/Coq/root @@ -1,2 +1 @@ baseuri=cic:/matita/procedural/Coq -include_paths=../../../legacy -- 2.39.2