- 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