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

diff --git a/helm/software/components/cic_proof_checking/cicDischarge.ml b/helm/software/components/cic_proof_checking/cicDischarge.ml
index 4ad41eef774913594c15f865c304c74ce07e92a2..65b5cea3393918525b68a721f7713b39955f32a0 100644 (file)
--- 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 7d6f630f4ace6a8af204b552871de3112aab5d78..2e2790a97fb9c3c45604180b80e7a0162ce5cce0 100644 (file)
--- 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 93dcd84fec668b31f5cfb9bb65db225033941bba..4bca3ab2833a7744fffaf7380e0613653af831d9 100644 (file)
--- 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 a5875f573e0ed26e805637edc9f1a7e85dcc738b..04d88dc07bf12e93dd654841e619709c635caebb 100644 (file)
--- 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 50d22b01376fb2298b36182616cf24227c0819a1..15286f493990c0ac8e86f434b5728351ccda6c30 100644 (file)
--- 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