Coq Extension

(*
NoConfusion_Foo (P : Type) [indices] (u v : Foo [indices]) :=
 match u, v with
 | Foo x y z, Foo x y z => (x == x' -> y == y' -> z == z' -> P) -> P
 | ...
 | Chalk*, Cheese* => P
 end
*)

(*
noConfusion_Foo (P : Type) [indices] (u v : Foo [indices]) : u == v -> NoConfusion_foo P [indices] u v.
*)

open Univ
open Inductive
open Util
open Coqlib

let ith_univ i = make_univ (make_dirpath [id_of_string"implicit"], i)
let implicit_type i = mkSort (Type (ith_univ i))
let raw_type i = RSort (dummy_loc, RType (Some (ith_univ i)))

let coq_heq_ref = lazy (Coqlib.coq_reference "mkHEq" ["Logic";"JMeq"] "JMeq")

let construct_no_conf_body env ind mind =
  let ctr_types = arities_of_constructors ind mind in
  let n_ctr_types = Array.length ctr_types in
  let n_indices = length (snd mind).mind_arity_ctxt in
  let indices =
    let rec names i = if i > n_indices then [] else RVar (dummy_loc, id_of_string ("e"^string_of_int i)) :: names (i+1) in names 1 in
  let abstract_indices x =
    let rec abs i =
      if i > n_indices
       then x
       else RLambda (dummy_loc, Name (id_of_string ("e"^string_of_int i)), Explicit, RHole (dummy_loc, BinderType Anonymous), abs (i+1)) in
    abs 1 in
  Pretyping.Default.understand Evd.empty env
   (RLambda (dummy_loc, Name (id_of_string "P"), Explicit, raw_type 1,
   abstract_indices
   (RLambda (dummy_loc, Name (id_of_string "u"), Explicit, RApp (dummy_loc, RRef (dummy_loc, IndRef ind), indices),
   (RLambda (dummy_loc, Name (id_of_string "v"), Explicit, RApp (dummy_loc, RRef (dummy_loc, IndRef ind), indices),
     RCases (dummy_loc, MatchStyle, None,
       [(RVar (dummy_loc, (id_of_string "u")), (Anonymous, None));(RVar (dummy_loc, (id_of_string "v")), (Anonymous, None))],
       (Array.to_list (Array.mapi (fun i ty_i ->
         let ctr = (ind, i+1) in
         let ctr_args = constructor_nrealhyps env ctr in
         let rec spread n i = if i = 0 then [] else (PatVar (dummy_loc, Name (id_of_string (n^string_of_int i)))) :: spread n (i-1) in
         let left_patterns = List.rev (spread "i" ctr_args) in
         let right_patterns = List.rev (spread "j" ctr_args) in
         let rec assume_eqs n x = if n > ctr_args
                                   then x
                                   else RProd (dummy_loc, Anonymous, Explicit,
                                        RApp (dummy_loc, RRef (dummy_loc, Lazy.force coq_heq_ref),
                                          [RHole (dummy_loc, BinderType Anonymous); RVar (dummy_loc, id_of_string ("i"^string_of_int n));
                                           RHole (dummy_loc, BinderType Anonymous); RVar (dummy_loc, id_of_string ("j"^string_of_int n))]),
                                        assume_eqs (n+1) x) in
         (dummy_loc, [id_of_string "foo";id_of_string "bar"],
                     [PatCstr (dummy_loc, ctr, left_patterns, Anonymous);PatCstr (dummy_loc, ctr, right_patterns, Anonymous)],
                     RProd (dummy_loc, Anonymous, Explicit,
                       assume_eqs 1 (RVar (dummy_loc, id_of_string "P")), RVar (dummy_loc, id_of_string "P")))) ctr_types) @
        if n_ctr_types = 1
         then []
         else [(dummy_loc, [id_of_string "foo";id_of_string "bar"],
                           [PatVar (dummy_loc, Anonymous);PatVar (dummy_loc, Anonymous)],
                           RVar (dummy_loc, id_of_string "P"))]))))))))

let construct_no_conf_declaration env ind mind =
 DefinitionEntry
  { const_entry_body = construct_no_conf_body env ind mind;
    const_entry_type = None;
    const_entry_opaque = false;
    const_entry_boxed = false }, IsDefinition Definition

let construct_little_no_conf env ind mind little_no_conf no_conf =
  let n_indices = length (snd mind).mind_arity_ctxt in
  let indices =
    let rec names i = if i > n_indices then [] else RVar (dummy_loc, id_of_string ("e"^string_of_int i)) :: names (i+1) in names 1 in
  let abstract_indices x =
    let rec abs i =
      if i > n_indices
       then x
       else RProd (dummy_loc, Name (id_of_string ("e"^string_of_int i)), Explicit, RHole (dummy_loc, BinderType Anonymous), abs (i+1)) in
    abs 1 in
  let little_no_conf_type = Pretyping.Default.understand Evd.empty env 
     (RProd (dummy_loc, Name (id_of_string "P"), Explicit, raw_type 1,
      abstract_indices
     (RProd (dummy_loc, Name (id_of_string "u"), Explicit, RApp (dummy_loc, RRef (dummy_loc, IndRef ind), indices),
     (RProd (dummy_loc, Name (id_of_string "v"), Explicit, RApp (dummy_loc, RRef (dummy_loc, IndRef ind), indices),
     (RProd (dummy_loc, Name (id_of_string "eql"), Explicit,
                          RApp (dummy_loc, RRef (dummy_loc, Lazy.force coq_heq_ref),
                           [RHole (dummy_loc, BinderType Anonymous); RVar (dummy_loc, id_of_string "u");
                            RHole (dummy_loc, BinderType Anonymous); RVar (dummy_loc, id_of_string "v")]),
       RApp (dummy_loc, RRef (dummy_loc, no_conf),
        ([RVar (dummy_loc, id_of_string "P")] @
         indices @
         [RVar (dummy_loc, id_of_string "u");
          RVar (dummy_loc, id_of_string "v")])))))))))) in
  try
    let _ =
    Pfedit.start_proof little_no_conf (Global, DefinitionBody Definition)
      (named_context_val env)
      little_no_conf_type
      (fun _ _ -> ());
    Pfedit.by (tclTHENSEQ
      [intros;
       simplest_elim (mkVar (id_of_string "eql"));
       simplest_elim (mkVar (id_of_string "u"));
       simpl_in_concl;
       Tauto.tauto]) in
    let _,(const,_,_) = Pfedit.cook_proof (fun _ -> ()) in
     Pfedit.delete_current_proof ();
     DefinitionEntry const, IsDefinition Definition
  with e ->
    Pfedit.delete_current_proof ();
    msg (str "Could not prove noConfusion, this is a serious (unexpected) problem!");
    raise e

let no_confusion i =
  check_required_library ["Coq";"Logic";"JMeq"];
  let env = Global.env () in
  let istr = string_of_id i in
  try
    match Nametab.locate (qualid_of_string istr) with
    | IndRef ind ->
       let mind = lookup_mind_specif env ind in
            let no_conf = add_prefix "NoConfusion_" i in
            let little_no_conf = add_prefix "noConfusion_" i in
            (* msg (print_constr (construct_no_conf_body env ind mind)); TODO: Print a better message *)
            let _ = Declare.declare_constant no_conf (construct_no_conf_declaration env ind mind) in
            let no_conf_ty = Nametab.locate (qualid_of_string ("NoConfusion_"^istr)) in
            let env = Global.env () in
            Declare.declare_constant little_no_conf (construct_little_no_conf env ind mind little_no_conf no_conf_ty);
            ()
    | _ -> msg (str (istr^" is not an inductive."))
  with Not_found -> msg (str ("Inductive "^istr^" not found in global environment."))
 

VERNAC COMMAND EXTEND Derive_NoConfusion
| [ "Derive" "NoConfusion" ident(i) ] -> [ no_confusion i ]
END