Source file `contradiction.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Constr
open EConstr
open Hipattern
open Tactics
open Reductionops
open Proofview.Notations

module NamedDecl = Context.Named.Declaration

(* Absurd *)

let mk_absurd_proof env r t =
  Tacticals.pf_constr_of_global (Coqlib.(lib_ref "core.not.type")) >>= fun coq_not ->
  Refine.refine ~typecheck:true begin fun sigma ->
    let sigma, negev = Evarutil.new_evar env sigma (mkApp (coq_not, [|t|])) in
    let sigma, ev = Evarutil.new_evar ~relevance:r env sigma t in
    sigma, mkApp (negev, [|ev|])
  end

let absurd c =
  Proofview.Goal.enter begin fun gl ->
    let sigma = Proofview.Goal.sigma gl in
    let env = Proofview.Goal.env gl in
    let j = Retyping.get_judgment_of env sigma c in
    let sigma, j = Coercion.inh_coerce_to_sort env sigma j in
    let t = nf_betaiota env sigma j.Environ.utj_val in
    let r = ESorts.relevance_of_sort j.Environ.utj_type in
    Proofview.Unsafe.tclEVARS sigma <*>
    Tactics.exfalso <*> mk_absurd_proof env r t
  end

let absurd c = absurd c

(* Contradiction *)

(** [f] does not assume its argument to be [nf_evar]-ed. *)
let filter_hyp f tac =
  let rec seek = function
    | [] ->
      let info = Exninfo.reify () in
      Proofview.tclZERO ~info Not_found
    | d::rest when f (NamedDecl.get_type d) -> tac (NamedDecl.get_id d)
    | _::rest -> seek rest in
  Proofview.Goal.enter begin fun gl ->
    let hyps = Proofview.Goal.hyps gl in
    seek hyps
  end

let contradiction_context =
  Proofview.Goal.enter begin fun gl ->
    let sigma = Tacmach.project gl in
    let env = Proofview.Goal.env gl in
    let rec seek_neg l = match l with
      | [] ->
        let info = Exninfo.reify () in
        Tacticals.tclZEROMSG ~info (Pp.str"No such contradiction")
      | d :: rest ->
          let id = NamedDecl.get_id d in
          let typ = nf_evar sigma (NamedDecl.get_type d) in
          let typ = whd_all env sigma typ in
          if is_empty_type env sigma typ then
            simplest_elim (mkVar id)
          else match EConstr.kind sigma typ with
          | Prod (na,t,u) when is_empty_type env sigma u ->
             let is_unit_or_eq = match_with_unit_or_eq_type env sigma t in
             Tacticals.tclORELSE
               (match is_unit_or_eq with
               | Some _ ->
                   let hd,args = decompose_app_list sigma t in
                   let (ind,_ as indu) = destInd sigma hd in
                   let nparams = Inductiveops.inductive_nparams env ind in
                   let params = Util.List.firstn nparams args in
                   let p = applist ((mkConstructUi (indu,1)), params) in
                   (* Checking on the fly that it type-checks *)
                   simplest_elim (mkApp (mkVar id,[|p|]))
               | None ->
                 let info = Exninfo.reify () in
                 Tacticals.tclZEROMSG ~info (Pp.str"Not a negated unit type."))
              (Proofview.tclORELSE
                 (Proofview.Goal.enter begin fun gl ->
                   let is_conv_leq = Tacmach.pf_apply is_conv_leq gl in
                   filter_hyp (fun typ -> is_conv_leq typ t)
                     (fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|])))
                 end)
                 begin function (e, info) -> match e with
                   | Not_found -> seek_neg rest
                   | e -> Proofview.tclZERO ~info e
                 end)
          | _ -> seek_neg rest
    in
    let hyps = Proofview.Goal.hyps gl in
    seek_neg hyps
  end

let is_negation_of env sigma typ t =
  match EConstr.kind sigma (whd_all env sigma t) with
    | Prod (na,t,u) ->
      is_empty_type env sigma u && is_conv_leq env sigma typ t
    | _ -> false

let contradiction_term (c,lbind as cl) =
  Proofview.Goal.enter begin fun gl ->
    let sigma = Tacmach.project gl in
    let env = Proofview.Goal.env gl in
    let typ = Tacmach.pf_get_type_of gl c in
    let _, ccl = whd_decompose_prod env sigma typ in
    if is_empty_type env sigma ccl then
      Tacticals.tclTHEN
        (elim false None cl None)
        (Tacticals.tclTRY assumption)
    else
      Proofview.tclORELSE
        begin
          if lbind = Tactypes.NoBindings then
            filter_hyp (fun c -> is_negation_of env sigma typ c)
              (fun id -> simplest_elim (mkApp (mkVar id,[|c|])))
          else
            let info = Exninfo.reify () in
            Proofview.tclZERO ~info Not_found
        end
        begin function (e, info) -> match e with
          | Not_found ->
            Tacticals.tclZEROMSG ~info (Pp.str"Not a contradiction.")
          | e -> Proofview.tclZERO ~info e
        end
  end

let contradiction = function
  | None -> Tacticals.tclTHEN intros contradiction_context
  | Some c -> contradiction_term c