Coverage report

(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* This file is the interface between the c-c algorithm and Coq *)

open Evd
open Names
open Inductiveops
open Declarations
open Constr
open EConstr
open Vars
open Tactics
open Typing
open Ccalgo
open Ccproof
open Pp
open Util
open Proofview.Notations

module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration

let reference dir s = lazy (Coqlib.coq_reference "CC" dir s)

let _f_equal = reference ["Init";"Logic"] "f_equal"
let _eq_rect = reference ["Init";"Logic"] "eq_rect"
let _refl_equal = reference ["Init";"Logic"] "eq_refl"
let _sym_eq = reference ["Init";"Logic"] "eq_sym"
let _trans_eq = reference ["Init";"Logic"] "eq_trans"
let _eq = reference ["Init";"Logic"] "eq"
let _False = reference ["Init";"Logic"] "False"
let _True = reference ["Init";"Logic"] "True"
let _I = reference ["Init";"Logic"] "I"

let whd env sigma t =
  Reductionops.clos_whd_flags CClosure.betaiotazeta env sigma t

let whd_delta env sigma t =
  Reductionops.clos_whd_flags CClosure.all env sigma t

(* decompose member of equality in an applicative format *)

(** FIXME: evar leak *)
let sf_of env sigma c = e_sort_of env (ref sigma) c

let rec decompose_term env sigma t=
    match EConstr.kind sigma (whd env sigma t) with
      App (f,args)->
        let tf=decompose_term env sigma f in
        let targs=Array.map (decompose_term env sigma) args in
          Array.fold_left (fun s t->Appli (s,t)) tf targs
    | Prod (_,a,_b) when noccurn sigma 1 _b ->
        let b = Termops.pop _b in
        let sort_b = sf_of env sigma b in
        let sort_a = sf_of env sigma a in
        Appli(Appli(Product (sort_a,sort_b) ,
                    decompose_term env sigma a),
              decompose_term env sigma b)
    | Construct c ->
        let (((mind,i_ind),i_con),u)= c in 
        let u = EInstance.kind sigma u in
        let canon_mind = MutInd.make1 (MutInd.canonical mind) in
        let canon_ind = canon_mind,i_ind in
        let (oib,_)=Global.lookup_inductive (canon_ind) in
        let nargs=constructor_nallargs_env env (canon_ind,i_con) in
          Constructor {ci_constr= ((canon_ind,i_con),u);
                       ci_arity=nargs;
                       ci_nhyps=nargs-oib.mind_nparams}
    | Ind c -> 
        let (mind,i_ind),u = c in 
        let u = EInstance.kind sigma u in
        let canon_mind = MutInd.make1 (MutInd.canonical mind) in
        let canon_ind = canon_mind,i_ind in  (Symb (Constr.mkIndU (canon_ind,u)))
    | Const (c,u) -> 
        let u = EInstance.kind sigma u in
        let canon_const = Constant.make1 (Constant.canonical c) in 
          (Symb (Constr.mkConstU (canon_const,u)))
    | Proj (p, c) -> 
        let canon_const kn = Constant.make1 (Constant.canonical kn) in 
        let p' = Projection.map canon_const p in
        let c = Retyping.expand_projection env sigma p' c [] in
        decompose_term env sigma c
    | _ ->
       let t = Termops.strip_outer_cast sigma t in
       if closed0 sigma t then Symb (EConstr.to_constr sigma t) else raise Not_found

(* decompose equality in members and type *)
open Termops

let atom_of_constr env sigma term =
  let wh = whd_delta env sigma term in
  let kot = EConstr.kind sigma wh in
    match kot with
      App (f,args)->
        if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3
          then `Eq (args.(0),
                   decompose_term env sigma args.(1),
                   decompose_term env sigma args.(2))
          else `Other (decompose_term env sigma term)
    | _ -> `Other (decompose_term env sigma term)

let rec pattern_of_constr env sigma c =
  match EConstr.kind sigma (whd env sigma c) with
      App (f,args)->
        let pf = decompose_term env sigma f in
        let pargs,lrels = List.split
          (Array.map_to_list (pattern_of_constr env sigma) args) in
          PApp (pf,List.rev pargs),
        List.fold_left Int.Set.union Int.Set.empty lrels
    | Prod (_,a,_b) when noccurn sigma 1 _b ->
        let b = Termops.pop _b in
        let pa,sa = pattern_of_constr env sigma a in
        let pb,sb = pattern_of_constr env sigma b in
        let sort_b = sf_of env sigma b in
        let sort_a = sf_of env sigma a in
          PApp(Product (sort_a,sort_b),
               [pa;pb]),(Int.Set.union sa sb)
    | Rel i -> PVar i,Int.Set.singleton i
    | _ ->
        let pf = decompose_term env sigma c in
          PApp (pf,[]),Int.Set.empty

let non_trivial = function
    PVar _ -> false
  | _ -> true

let patterns_of_constr env sigma nrels term=
  let f,args=
    try destApp sigma (whd_delta env sigma term) with DestKO -> raise Not_found in
        if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3
        then
          let patt1,rels1 = pattern_of_constr env sigma args.(1)
          and patt2,rels2 = pattern_of_constr env sigma args.(2) in
          let valid1 =
            if not (Int.equal (Int.Set.cardinal rels1) nrels) then Creates_variables
            else if non_trivial patt1 then Normal
            else Trivial (EConstr.to_constr sigma args.(0))
          and valid2 =
            if not (Int.equal (Int.Set.cardinal rels2) nrels) then Creates_variables
            else if non_trivial patt2 then Normal
            else Trivial (EConstr.to_constr sigma args.(0)) in
            if valid1 != Creates_variables
              || valid2 != Creates_variables  then
              nrels,valid1,patt1,valid2,patt2
            else raise Not_found
        else raise Not_found

let rec quantified_atom_of_constr env sigma nrels term =
  match EConstr.kind sigma (whd_delta env sigma term) with
      Prod (id,atom,ff) -> 
        if is_global sigma (Lazy.force _False) ff then
          let patts=patterns_of_constr env sigma nrels atom in
              `Nrule patts
        else 
          quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma (succ nrels) ff
    | _ ->  
        let patts=patterns_of_constr env sigma nrels term in
            `Rule patts

let litteral_of_constr env sigma term=
  match EConstr.kind sigma (whd_delta env sigma term) with
    | Prod (id,atom,ff) -> 
        if is_global sigma (Lazy.force _False) ff then
          match (atom_of_constr env sigma atom) with
              `Eq(t,a,b) -> `Neq(t,a,b)
            | `Other(p) -> `Nother(p)
        else
          begin
            try 
              quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma 1 ff
            with Not_found ->
              `Other (decompose_term env sigma term)
          end
    | _ ->
        atom_of_constr env sigma term


(* store all equalities from the context *)

let make_prb gls depth additionnal_terms =
  let open Tacmach.New in
  let env=pf_env gls in
  let sigma=project gls in
  let state = empty depth {it = Proofview.Goal.goal (Proofview.Goal.assume gls); sigma } in
  let pos_hyps = ref [] in
  let neg_hyps =ref [] in
    List.iter
      (fun c ->
         let t = decompose_term env sigma c in
           ignore (add_term state t)) additionnal_terms;
    List.iter
      (fun decl ->
         let id = NamedDecl.get_id decl in
         begin
           let cid=Constr.mkVar id in
           match litteral_of_constr env sigma (NamedDecl.get_type decl) with
               `Eq (t,a,b) -> add_equality state cid a b
             | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b
             | `Other ph ->
                 List.iter
                   (fun (cidn,nh) ->
                      add_disequality state (HeqnH (cid,cidn)) ph nh)
                   !neg_hyps;
                 pos_hyps:=(cid,ph):: !pos_hyps
             | `Nother nh ->
                 List.iter
                   (fun (cidp,ph) ->
                      add_disequality state (HeqnH (cidp,cid)) ph nh)
                   !pos_hyps;
                 neg_hyps:=(cid,nh):: !neg_hyps
             | `Rule patts -> add_quant state id true patts
             | `Nrule patts -> add_quant state id false patts
         end) (Proofview.Goal.hyps gls);
    begin
      match atom_of_constr env sigma (pf_concl gls) with
          `Eq (t,a,b) -> add_disequality state Goal a b
        |        `Other g ->
                  List.iter
              (fun (idp,ph) ->
                 add_disequality state (HeqG idp) ph g) !pos_hyps
    end;
    state

(* indhyps builds the array of arrays of constructor hyps for (ind largs) *)

let build_projection intype (cstr:pconstructor) special default gls=
  let open Tacmach.New in
  let ci= (snd(fst cstr)) in
  let sigma = project gls in
  let body=Equality.build_selector (pf_env gls) sigma ci (mkRel 1) intype special default in
  let id=pf_get_new_id (Id.of_string "t") gls in
  sigma, mkLambda(Name id,intype,body)

(* generate an adhoc tactic following the proof tree  *)

let app_global f args k =
  Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc -> k (mkApp (fc, args))

let rec gen_holes env sigma t n accu =
  if Int.equal n 0 then (sigma, List.rev accu)
  else match EConstr.kind sigma t with
  | Prod (_, u, t) ->
    let (sigma, ev) = Evarutil.new_evar env sigma u in
    let t = EConstr.Vars.subst1 ev t in
    gen_holes env sigma t (pred n) (ev :: accu)
  | _ -> assert false

let app_global_with_holes f args n =
  Proofview.Goal.enter begin fun gl ->
    Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc ->
    let env = Proofview.Goal.env gl in
    let concl = Proofview.Goal.concl gl in
    Refine.refine ~typecheck:false begin fun sigma ->
      let t = Tacmach.New.pf_get_type_of gl fc in
      let t = Termops.prod_applist sigma t (Array.to_list args) in
      let ans = mkApp (fc, args) in
      let (sigma, holes) = gen_holes env sigma t n [] in
      let ans = applist (ans, holes) in
      let evdref = ref sigma in
      let () = Typing.e_check env evdref ans concl in
      (!evdref, ans)
    end
  end

let assert_before n c =
  Proofview.Goal.enter begin fun gl ->
    let evm, _ = Tacmach.New.pf_apply type_of gl c in
    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm)
    (assert_before n c)
  end

let refresh_type env evm ty =
  Evarsolve.refresh_universes ~status:Evd.univ_flexible ~refreshset:true
                              (Some false) env evm ty

let refresh_universes ty k =
  Proofview.Goal.enter begin fun gl ->
    let env = Proofview.Goal.env gl in
    let evm = Tacmach.New.project gl in
    let evm, ty = refresh_type env evm ty in
    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm) (k ty)
  end

let constr_of_term c = EConstr.of_constr (constr_of_term c)

let rec proof_tac p : unit Proofview.tactic =
  Proofview.Goal.enter begin fun gl ->
  let type_of t = Tacmach.New.pf_unsafe_type_of gl t in
  try (* type_of can raise exceptions *)
  match p.p_rule with
      Ax c -> exact_check (EConstr.of_constr c)
    | SymAx c ->
        let c = EConstr.of_constr c in
        let l=constr_of_term p.p_lhs and
            r=constr_of_term p.p_rhs in
        refresh_universes (type_of l) (fun typ ->
        app_global _sym_eq [|typ;r;l;c|] exact_check)
    | Refl t ->
        let lr = constr_of_term t in
        refresh_universes (type_of lr) (fun typ ->
        app_global _refl_equal [|typ;constr_of_term t|] exact_check)
    | Trans (p1,p2)->
        let t1 = constr_of_term p1.p_lhs and
            t2 = constr_of_term p1.p_rhs and
            t3 = constr_of_term p2.p_rhs in
        refresh_universes (type_of t2) (fun typ ->
        let prf = app_global_with_holes _trans_eq [|typ;t1;t2;t3;|] 2 in
          Tacticals.New.tclTHENS prf [(proof_tac p1);(proof_tac p2)])
    | Congr (p1,p2)->
        let tf1=constr_of_term p1.p_lhs
        and tx1=constr_of_term p2.p_lhs
        and tf2=constr_of_term p1.p_rhs
        and tx2=constr_of_term p2.p_rhs in
        refresh_universes (type_of tf1) (fun typf ->
        refresh_universes (type_of tx1) (fun typx ->
        refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx ->
        let id = Tacmach.New.pf_get_new_id (Id.of_string "f") gl in
        let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
        let lemma1 = app_global_with_holes _f_equal [|typf;typfx;appx1;tf1;tf2|] 1 in
        let lemma2 = app_global_with_holes _f_equal [|typx;typfx;tf2;tx1;tx2|] 1 in
        let prf =
          app_global_with_holes _trans_eq
                [|typfx;
                  mkApp(tf1,[|tx1|]);
                  mkApp(tf2,[|tx1|]);
                  mkApp(tf2,[|tx2|])|] 2 in
          Tacticals.New.tclTHENS prf
            [Tacticals.New.tclTHEN lemma1 (proof_tac p1);
               Tacticals.New.tclFIRST
               [Tacticals.New.tclTHEN lemma2 (proof_tac p2);
                reflexivity;
                Tacticals.New.tclZEROMSG
                    (Pp.str
                       "I don't know how to handle dependent equality")]])))
  | Inject (prf,cstr,nargs,argind) ->
         let ti=constr_of_term prf.p_lhs in
         let tj=constr_of_term prf.p_rhs in
         let default=constr_of_term p.p_lhs in
         let special=mkRel (1+nargs-argind) in
         refresh_universes (type_of ti) (fun intype ->
         refresh_universes (type_of default) (fun outtype ->
         let sigma, proj =
           build_projection intype cstr special default gl
         in
         let injt=
           app_global_with_holes _f_equal [|intype;outtype;proj;ti;tj|] 1 in
         Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
                               (Tacticals.New.tclTHEN injt (proof_tac prf))))
  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
  end

let refute_tac c t1 t2 p =
  Proofview.Goal.enter begin fun gl ->
  let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
  let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in
  let false_t=mkApp (c,[|mkVar hid|]) in
  let k intype =
    let neweq= app_global _eq [|intype;tt1;tt2|] in
    Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
      [proof_tac p; simplest_elim false_t]
  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k
  end

let refine_exact_check c =
  Proofview.Goal.enter begin fun gl ->
    let evm, _ = Tacmach.New.pf_apply type_of gl c in
    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm) (exact_check c)
  end

let convert_to_goal_tac c t1 t2 p = 
  Proofview.Goal.enter begin fun gl ->
  let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
  let k sort =
    let neweq= app_global _eq [|sort;tt1;tt2|] in
    let e = Tacmach.New.pf_get_new_id (Id.of_string "e") gl in
    let x = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in
    let identity=mkLambda (Name x,sort,mkRel 1) in
    let endt = app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
    Tacticals.New.tclTHENS (neweq (assert_before (Name e)))
                           [proof_tac p; endt refine_exact_check]
  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k
  end

let convert_to_hyp_tac c1 t1 c2 t2 p =
  Proofview.Goal.enter begin fun gl ->
  let tt2=constr_of_term t2 in
  let h = Tacmach.New.pf_get_new_id (Id.of_string "H") gl in
  let false_t=mkApp (c2,[|mkVar h|]) in
    Tacticals.New.tclTHENS (assert_before (Name h) tt2)
      [convert_to_goal_tac c1 t1 t2 p;
       simplest_elim false_t]
  end

(* Essentially [assert (Heq : lhs = rhs) by proof_tac p; discriminate Heq] *)
let discriminate_tac cstru p =
  Proofview.Goal.enter begin fun gl ->
    let lhs=constr_of_term p.p_lhs and rhs=constr_of_term p.p_rhs in
    let env = Proofview.Goal.env gl in
    let evm = Tacmach.New.project gl in
    let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl lhs) in
    let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in
    let neweq=app_global _eq [|intype;lhs;rhs|] in
    Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm)
                          (Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
      [proof_tac p; Equality.discrHyp hid])
  end

(* wrap everything *)

let build_term_to_complete uf pac =
  let cinfo = get_constructor_info uf pac.cnode in
  let real_args = List.rev_map (fun i -> constr_of_term (term uf i)) pac.args in
  let (kn, u) = cinfo.ci_constr in
  (applist (mkConstructU (kn, EInstance.make u), real_args), pac.arity)

let cc_tactic depth additionnal_terms =
  Proofview.Goal.enter begin fun gl ->
    let sigma = Tacmach.New.project gl in
    Coqlib.check_required_library Coqlib.logic_module_name;
    let _ = debug (fun () -> Pp.str "Reading subgoal ...") in
    let state = make_prb gl depth additionnal_terms in
    let _ = debug (fun () -> Pp.str "Problem built, solving ...") in
    let sol = execute true state in
    let _ = debug (fun () -> Pp.str "Computation completed.") in
    let uf=forest state in
    match sol with
      None -> Tacticals.New.tclFAIL 0 (str "congruence failed")
    | Some reason ->
        debug (fun () -> Pp.str "Goal solved, generating proof ...");
        match reason with
          Discrimination (i,ipac,j,jpac) ->
            let p=build_proof uf (`Discr (i,ipac,j,jpac)) in
            let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
            discriminate_tac cstr p
        | Incomplete ->
            let open Glob_term in
            let env = Proofview.Goal.env gl in
            let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in
            let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in
            let pr_missing (c, missing) =
              let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in
              let holes = List.init missing (fun _ -> hole) in
              Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes))
            in
            Feedback.msg_info
              (Pp.str "Goal is solvable by congruence but some arguments are missing.");
            Feedback.msg_info
              (Pp.str "  Try " ++
                 hov 8
                 begin
                   str "\"congruence with (" ++
                     prlist_with_sep
                     (fun () -> str ")" ++ spc () ++ str "(")
                     pr_missing
                     terms_to_complete ++
                     str ")\","
                 end ++
                 Pp.str "  replacing metavariables by arbitrary terms.");
            Tacticals.New.tclFAIL 0 (str "Incomplete")
        | Contradiction dis ->
            let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in
            let ta=term uf dis.lhs and tb=term uf dis.rhs in
            match dis.rule with
              Goal -> proof_tac p
            | Hyp id -> refute_tac (EConstr.of_constr id) ta tb p
            | HeqG id ->
                let id = EConstr.of_constr id in
                convert_to_goal_tac id ta tb p
            | HeqnH (ida,idb) ->
                let ida = EConstr.of_constr ida in
                let idb = EConstr.of_constr idb in
                convert_to_hyp_tac ida ta idb tb p
  end

let cc_fail =
  Tacticals.New.tclZEROMSG (Pp.str "congruence failed.")

let congruence_tac depth l =
  Tacticals.New.tclORELSE
    (Tacticals.New.tclTHEN (Tacticals.New.tclREPEAT introf) (cc_tactic depth l))
    cc_fail

(* Beware: reflexivity = constructor 1 = apply refl_equal
   might be slow now, let's rather do something equivalent
   to a "simple apply refl_equal" *)

(* The [f_equal] tactic.

   It mimics the use of lemmas [f_equal], [f_equal2], etc.
   This isn't particularly related with congruence, apart from
   the fact that congruence is called internally.
*)

let mk_eq f c1 c2 k =
  Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc ->
  Proofview.Goal.enter begin fun gl ->
    let open Tacmach.New in
    let evm, ty = pf_apply type_of gl c1 in
    let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in
    let term = mkApp (fc, [| ty; c1; c2 |]) in
    let evm, _ =  type_of (pf_env gl) evm term in
    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm) (k term)
    end

let f_equal =
  Proofview.Goal.enter begin fun gl ->
    let concl = Proofview.Goal.concl gl in
    let sigma = Tacmach.New.project gl in
    let cut_eq c1 c2 =
      try (* type_of can raise an exception *)
        Tacticals.New.tclTHENS
          (mk_eq _eq c1 c2 Tactics.cut)
          [Proofview.tclUNIT ();Tacticals.New.tclTRY ((app_global _refl_equal [||]) apply)]
      with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
    in
    Proofview.tclORELSE
      begin match EConstr.kind sigma concl with
      | App (r,[|_;t;t'|]) when is_global sigma (Lazy.force _eq) r ->
          begin match EConstr.kind sigma t, EConstr.kind sigma t' with
          | App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') ->
              let rec cuts i =
                if i < 0 then Tacticals.New.tclTRY (congruence_tac 1000 [])
                else Tacticals.New.tclTHENFIRST (cut_eq v.(i) v'.(i)) (cuts (i-1))
              in cuts (Array.length v - 1)
          | _ -> Proofview.tclUNIT ()
          end
      | _ -> Proofview.tclUNIT ()
      end
      begin function (e, info) -> match e with
        | Pretype_errors.PretypeError _ | Type_errors.TypeError _ -> Proofview.tclUNIT ()
        | e -> Proofview.tclZERO ~info e
      end
  end
plugins/cc/cctac.ml

89.98%
