package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file derive.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
(************************************************************************)
(*         *   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 Context
open Context.Named.Declaration

(** [start_deriving f suchthat lemma] starts a proof of [suchthat]
    (which can contain references to [f]) in the context extended by
    [f:=?x]. When the proof ends, [f] is defined as the value of [?x]
    and [lemma] as the proof. *)
let start_deriving f suchthat name : Declare.Proof.t =

  let env = Global.env () in
  let sigma = Evd.from_env env in
  let poly = false in
  let kind = Decls.(IsDefinition Definition) in

  (* create a sort variable for the type of [f] *)
  (* spiwack: I don't know what the rigidity flag does, picked the one
     that looked the most general. *)
  let (sigma,f_type_sort) = Evd.new_sort_variable Evd.univ_flexible_alg sigma in
  let f_type_type = EConstr.mkSort f_type_sort in
  (* create the initial goals for the proof: |- Type ; |- ?1 ; f:=?2 |- suchthat *)
  let goals =
    let open Proofview in
    TCons ( env , sigma , f_type_type , (fun sigma f_type ->
        TCons ( env , sigma , f_type , (fun sigma ef ->
            let f_type = EConstr.Unsafe.to_constr f_type in
            let ef = EConstr.Unsafe.to_constr ef in
            let env' = Environ.push_named (LocalDef (annotR f, ef, f_type)) env in
            let sigma, suchthat = Constrintern.interp_type_evars ~program_mode:false env' sigma suchthat in
            TCons ( env' , sigma , suchthat , (fun sigma _ ->
                TNil sigma))))))
  in

  let info = Declare.Info.make ~poly ~kind () in
  let lemma = Declare.Proof.start_derive ~name ~f ~info goals in
  Declare.Proof.map lemma ~f:(fun p ->
      Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p)
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct