+let mk_sym uri ty t1 t2 p =
+ let ens, args = build_ens uri [ty;t1;t2;p] in
+ Cic.Appl (Cic.Const(uri, ens) :: args)
+;;
+
+let mk_trans uri ty t1 t2 t3 p12 p23 =
+ let ens, args = build_ens uri [ty;t1;t2;t3;p12;p23] in
+ Cic.Appl (Cic.Const (uri, ens) :: args)
+;;
+
+let mk_eq_ind uri ty what pred p1 other p2 =
+ Cic.Appl [Cic.Const (uri, []); ty; what; pred; p1; other; p2]
+;;
+
+let p_of_sym ens tl =
+ let args = List.map snd ens @ tl in
+ match args with
+ | [_;_;_;p] -> p
+ | _ -> assert false
+;;
+
+let open_trans ens tl =
+ let args = List.map snd ens @ tl in
+ match args with
+ | [ty;l;m;r;p1;p2] -> ty,l,m,r,p1,p2
+ | _ -> assert false
+;;
+
+let canonical t =
+ let rec remove_refl t =
+ match t with
+ | Cic.Appl (((Cic.Const(uri_trans,ens))::tl) as args)
+ when LibraryObjects.is_trans_eq_URI uri_trans ->
+ let ty,l,m,r,p1,p2 = open_trans ens tl in
+ (match p1,p2 with
+ | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_],p2 ->
+ remove_refl p2
+ | p1,Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] ->
+ remove_refl p1
+ | _ -> Cic.Appl (List.map remove_refl args))
+ | Cic.Appl l -> Cic.Appl (List.map remove_refl l)
+ | _ -> t
+ in
+ let rec canonical t =
+ match t with
+ | Cic.Appl (((Cic.Const(uri_sym,ens))::tl) as args)
+ when LibraryObjects.is_sym_eq_URI uri_sym ->
+ (match p_of_sym ens tl with
+ | Cic.Appl ((Cic.Const(uri,ens))::tl)
+ when LibraryObjects.is_sym_eq_URI uri ->
+ canonical (p_of_sym ens tl)
+ | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
+ when LibraryObjects.is_trans_eq_URI uri_trans ->
+ let ty,l,m,r,p1,p2 = open_trans ens tl in
+ mk_trans uri_trans ty r m l
+ (canonical (mk_sym uri_sym ty m r p2))
+ (canonical (mk_sym uri_sym ty l m p1))
+ | Cic.Appl (((Cic.Const(uri_ind,ens)) as he)::tl)
+ when LibraryObjects.is_eq_ind_URI uri_ind ||
+ LibraryObjects.is_eq_ind_r_URI uri_ind ->
+ let ty, what, pred, p1, other, p2 =
+ match tl with
+ | [ty;what;pred;p1;other;p2] -> ty, what, pred, p1, other, p2
+ | _ -> assert false
+ in
+ let pred,l,r =
+ match pred with
+ | Cic.Lambda (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;l;r])
+ when LibraryObjects.is_eq_URI uri ->
+ Cic.Lambda
+ (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;r;l]),l,r
+ | _ ->
+ prerr_endline (CicPp.ppterm pred);
+ assert false
+ in
+ let l = CicSubstitution.subst what l in
+ let r = CicSubstitution.subst what r in
+ Cic.Appl
+ [he;ty;what;pred;
+ canonical (mk_sym uri_sym ty l r p1);other;canonical p2]
+ | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] as t
+ when LibraryObjects.is_eq_URI uri -> t
+ | _ -> Cic.Appl (List.map canonical args))
+ | Cic.Appl l -> Cic.Appl (List.map canonical l)
+ | _ -> t
+ in
+ remove_refl (canonical t)
+;;
+
+let build_proof_step subst p1 p2 pos l r pred =
+ let p1 = apply_subst subst p1 in
+ let p2 = apply_subst subst p2 in
+ let l = apply_subst subst l in
+ let r = apply_subst subst r in
+ let pred = apply_subst subst pred in
+ let ty,body = (* Cic.Implicit None *)
+ match pred with
+ | Cic.Lambda (_,ty,body) -> ty,body
+ | _ -> assert false
+ in
+ let what, other = (* Cic.Implicit None, Cic.Implicit None *)
+ if pos = Utils.Left then l,r else r,l
+ in
+ let is_not_fixed t =
+ CicSubstitution.subst (Cic.Implicit None) t <>
+ CicSubstitution.subst (Cic.Rel 1) t
+ in
+ match body,pos with
+ |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Left ->
+ let third = CicSubstitution.subst (Cic.Implicit None) third in
+ let uri_trans = LibraryObjects.trans_eq_URI ~eq in
+ let uri_sym = LibraryObjects.sym_eq_URI ~eq in
+ mk_trans uri_trans ty other what third
+ (mk_sym uri_sym ty what other p2) p1
+ |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Right ->
+ let third = CicSubstitution.subst (Cic.Implicit None) third in
+ let uri_trans = LibraryObjects.trans_eq_URI ~eq in
+ mk_trans uri_trans ty other what third p2 p1
+ |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Left ->
+ let third = CicSubstitution.subst (Cic.Implicit None) third in
+ let uri_trans = LibraryObjects.trans_eq_URI ~eq in
+ mk_trans uri_trans ty third what other p1 p2
+ |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Right ->
+ let third = CicSubstitution.subst (Cic.Implicit None) third in
+ let uri_trans = LibraryObjects.trans_eq_URI ~eq in
+ let uri_sym = LibraryObjects.sym_eq_URI ~eq in
+ mk_trans uri_trans ty third what other p1
+ (mk_sym uri_sym ty other what p2)
+ | Cic.Appl [Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed lhs
+ ->
+ let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in
+ let uri_trans = LibraryObjects.trans_eq_URI ~eq in
+ let uri_sym = LibraryObjects.sym_eq_URI ~eq in
+ let pred_of t = CicSubstitution.subst t lhs in
+ let pred_of_what = pred_of what in
+ let pred_of_other = pred_of other in
+ (* p2 : what = other
+ * ====================================
+ * inject p2: P(what) = P(other)
+ *)
+ let inject ty lhs what other p2 =
+ let liftedty = CicSubstitution.lift 1 ty in
+ let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
+ let refl_eq_part =
+ Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
+ in
+ mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
+ (Cic.Lambda (Cic.Name "foo",ty,
+ (Cic.Appl
+ [Cic.MutInd(eq,0,[]);liftedty;lhs;lifted_pred_of_other])))
+ refl_eq_part what p2
+ in
+ mk_trans uri_trans ty pred_of_other pred_of_what rhs
+ (mk_sym uri_sym ty pred_of_what pred_of_other
+ (inject ty lhs what other p2)
+ ) p1
+ | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed lhs
+ ->
+ let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in
+ let uri_trans = LibraryObjects.trans_eq_URI ~eq in
+ let uri_sym = LibraryObjects.sym_eq_URI ~eq in
+ let pred_of t = CicSubstitution.subst t lhs in
+ let pred_of_what = pred_of what in
+ let pred_of_other = pred_of other in
+ (* p2 : what = other
+ * ====================================
+ * inject p2: P(what) = P(other)
+ *)
+ let inject ty lhs what other p2 =
+ let liftedty = CicSubstitution.lift 1 ty in
+ let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
+ let refl_eq_part =
+ Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
+ in
+ mk_eq_ind (Utils.eq_ind_URI ()) ty other
+ (Cic.Lambda (Cic.Name "foo",ty,
+ (Cic.Appl
+ [Cic.MutInd(eq,0,[]);liftedty;lhs;lifted_pred_of_other])))
+ refl_eq_part what p2
+ in
+ mk_trans uri_trans ty pred_of_other pred_of_what rhs
+ (mk_sym uri_sym ty pred_of_other pred_of_what
+ (inject ty lhs what other p2)
+ ) p1
+ | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed rhs
+ ->
+ let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
+ let uri_trans = LibraryObjects.trans_eq_URI ~eq in
+ let uri_sym = LibraryObjects.sym_eq_URI ~eq in
+ let pred_of t = CicSubstitution.subst t rhs in
+ let pred_of_what = pred_of what in
+ let pred_of_other = pred_of other in
+ (* p2 : what = other
+ * ====================================
+ * inject p2: P(what) = P(other)
+ *)
+ let inject ty lhs what other p2 =
+ let liftedty = CicSubstitution.lift 1 ty in
+ let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
+ let refl_eq_part =
+ Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
+ in
+ mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
+ (Cic.Lambda (Cic.Name "foo",ty,
+ (Cic.Appl
+ [Cic.MutInd(eq,0,[]);liftedty;lhs;lifted_pred_of_other])))
+ refl_eq_part what p2
+ in
+ mk_trans uri_trans ty lhs pred_of_what pred_of_other p1
+ (mk_sym uri_sym ty pred_of_what pred_of_other
+ (inject ty rhs other what p2))
+ | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed rhs
+ ->
+ let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
+ let uri_trans = LibraryObjects.trans_eq_URI ~eq in
+ let uri_sym = LibraryObjects.sym_eq_URI ~eq in
+ let pred_of t = CicSubstitution.subst t rhs in
+ let pred_of_what = pred_of what in
+ let pred_of_other = pred_of other in
+ (* p2 : what = other
+ * ====================================
+ * inject p2: P(what) = P(other)
+ *)
+ let inject ty lhs what other p2 =
+ let liftedty = CicSubstitution.lift 1 ty in
+ let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
+ let refl_eq_part =
+ Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
+ in
+ mk_eq_ind (Utils.eq_ind_URI ()) ty other
+ (Cic.Lambda (Cic.Name "foo",ty,
+ (Cic.Appl
+ [Cic.MutInd(eq,0,[]);liftedty;lhs;lifted_pred_of_other])))
+ refl_eq_part what p2
+ in
+ mk_trans uri_trans ty lhs pred_of_what pred_of_other p1
+ (mk_sym uri_sym ty pred_of_other pred_of_what
+ (inject ty rhs other what p2))
+ | _, Utils.Left ->
+ mk_eq_ind (Utils.eq_ind_URI ()) ty what pred p1 other p2
+ | _, Utils.Right ->
+ mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2
+;;
+