+ let dag =
+ let uri = NUri.uri_of_string "cic:/matita/ng/sets/setoids/prop1.con" in
+ let ref = NReference.reference_of_spec uri (NReference.Fix(0,2,4)) in
+ NCic.Const ref
+ ;;
+
+ (*
+ let eq_setoid =
+ let uri = NUri.uri_of_string "cic:/matita/ng/sets/setoids/eq.con" in
+ let ref = NReference.reference_of_spec uri (NReference.Fix(0,0,2)) in
+ NCic.Const ref
+ ;;
+ *)
+
+ let sym eq =
+ let u= NUri.uri_of_string "cic:/matita/ng/properties/relations/sym.con" in
+ let u = NReference.reference_of_spec u (NReference.Fix(0,1,3)) in
+ NCic.Appl[NCic.Const u; NCic.Implicit `Type; NCic.Implicit `Term;
+ NCic.Implicit `Term; NCic.Implicit `Term; eq];
+ ;;
+
+ let eq_morphism1 eq =
+ let u= NUri.uri_of_string "cic:/matita/ng/sets/setoids/eq_is_morphism1.con" in
+ let u = NReference.reference_of_spec u (NReference.Def 4) in
+ NCic.Appl[NCic.Const u; NCic.Implicit `Term; NCic.Implicit `Term;
+ NCic.Implicit `Term; NCic.Implicit `Term; eq];
+ ;;
+
+ let eq_morphism2 eq =
+ let u= NUri.uri_of_string "cic:/matita/ng/sets/setoids/eq_is_morphism2.con" in
+ let u = NReference.reference_of_spec u (NReference.Def 4) in
+ NCic.Appl[NCic.Const u; NCic.Implicit `Term; NCic.Implicit `Term;
+ NCic.Implicit `Term; eq; NCic.Implicit `Term];
+ ;;
+
+ let trans eq p =
+ let u= NUri.uri_of_string "cic:/matita/ng/properties/relations/trans.con" in
+ let u = NReference.reference_of_spec u (NReference.Fix(0,1,3)) in
+ NCic.Appl[NCic.Const u; NCic.Implicit `Type; NCic.Implicit `Term;
+ NCic.Implicit `Term; NCic.Implicit `Term; NCic.Implicit `Term; eq]
+ ;;
+
+ let iff1 eq p =
+ let uri = NUri.uri_of_string "cic:/matita/ng/logic/connectives/if.con" in
+ let ref = NReference.reference_of_spec uri (NReference.Fix(0,2,1)) in
+ NCic.Appl[NCic.Const ref; NCic.Implicit `Type; NCic.Implicit `Type;
+ eq; p];
+ ;;
+
+(*
+ let mk_refl = function
+ | NCic.Appl [_; _; x; _] ->
+ let uri= NUri.uri_of_string "cic:/matita/ng/properties/relations/refl.con" in
+ let ref = NReference.reference_of_spec uri (NReference.Fix(0,1,3)) in
+ NCic.Appl[NCic.Const ref; NCic.Implicit `Type; NCic.Implicit `Term;
+ NCic.Implicit `Term(*x*)]
+ | _ -> assert false
+*)
+
+ let mk_refl = function
+ | NCic.Appl [_; ty; l; _]
+ -> NCic.Appl [eq_refl();ty;l]
+ | _ -> assert false
+
+
+ let mk_morphism eq amount ft pl vl =
+ let rec aux t p =
+ match p with
+ | [] -> eq
+ | n::tl ->
+ prerr_endline (string_of_int n);
+ match t with
+ | Terms.Leaf _
+ | Terms.Var _ -> assert false
+ | Terms.Node [] -> assert false
+ | Terms.Node [ Terms.Leaf eqt ; _; l; r ]
+ when (eqP ()) = eqt ->
+ if n=2 then eq_morphism1 (aux l tl)
+ else eq_morphism2 (aux r tl)
+ | Terms.Node (f::l) ->
+ snd (
+ List.fold_left
+ (fun (i,acc) t ->
+ i+1,
+ let f = extract amount vl f in
+ if i = n then
+ let imp = NCic.Implicit `Term in
+ NCic.Appl (dag::imp::imp::imp(* f *)::imp::imp::
+ [aux t tl])
+ else
+ NCicUntrusted.mk_appl acc [extract amount vl t]
+ ) (1,extract amount vl f) l)
+ in aux ft (List.rev pl)
+ ;;
+
+ let mk_proof ?(demod=false) (bag : NCic.term Terms.bag) mp subst steps =
+ let module NCicBlob =
+ NCicBlob.NCicBlob(
+ struct
+ let metasenv = [] let subst = [] let context = []
+ end)
+ in
+ let module Pp = Pp.Pp(NCicBlob)
+ in