new proof terms

[c-cube]

• directly use twine for proofs
• use newer twine features like explicit offsets, to be able to read only one proof step at a time
• generate type for proof steps and deep proof steps
• add a proof writer

[c-cube]

The generated types.ml file:

(** Proof rules.

    Proof rules in use in ImandraX. *)

(* auto-generated in [gen/mk_rules.ml], do not modify *)

type 'a offset_for = 'a Imandrakit_twine.offset_for [@@deriving eq, show, twine, typereg]


(** A proof step, proving a clause using logical rules. *)
type proof_step =
  | Assume of Scope.t * Imandrax_api_mir.Term.t
  | By_def of Scope.t * Imandrax_api_mir.Term.t * Imandrax_api_mir.Term.t
  | Lemma of Scope.t * Imandrax_api_mir.Term.t * Imandrax_api_mir.Sequent.t
  | Sorry of Scope.t * Imandrax_api_mir.Sequent.t
  | Cc of Scope.t * Imandrax_api_mir.Sequent.t
  | Intros of Scope.t * Imandrax_api_mir.Sequent.t
  | Unintros of Scope.t * Imandrax_api_mir.Term.t list * Imandrax_api_mir.Sequent.t
  | If_true of Scope.t * Imandrax_api_mir.Term.t
  | If_false of Scope.t * Imandrax_api_mir.Term.t
  | If_trivial of Scope.t * Imandrax_api_mir.Term.t
  | If_trivial_neg of Scope.t * Imandrax_api_mir.Term.t
  | Trivial of Scope.t * Imandrax_api_mir.Sequent.t
  | And_elim of Scope.t * Imandrax_api_mir.Sequent.t * Imandrax_api_mir.Sequent.t
  | Or_left of Scope.t * Imandrax_api_mir.Sequent.t * Imandrax_api_mir.Term.t
  | Or_right of Scope.t * Imandrax_api_mir.Sequent.t * Imandrax_api_mir.Term.t
  | Cstor_inj of Scope.t * Imandrax_api_mir.Term.t * Imandrax_api_mir.Term.t * int
  | Cstor_disj of Scope.t * Imandrax_api_mir.Term.t * Imandrax_api_mir.Term.t
  | Cstor_is_a_true of Scope.t * Imandrax_api_mir.Term.t * Imandrax_api_mir.Term.t
  | Cstor_is_a_false of Scope.t * Imandrax_api_mir.Term.t * Imandrax_api_mir.Term.t
  | Cstor_is_a_project of Scope.t * Imandrax_api_mir.Term.t
  | Cstor_select of Scope.t * Imandrax_api_mir.Term.t * Imandrax_api_mir.Term.t
  | Destruct of Scope.t * Imandrax_api_mir.Term.t * Imandrax_api_mir.Term.t
  | And_true_left of Scope.t * Imandrax_api_mir.Term.t
  | And_true_right of Scope.t * Imandrax_api_mir.Term.t
  | And_false_left of Scope.t * Imandrax_api_mir.Term.t
  | And_false_right of Scope.t * Imandrax_api_mir.Term.t
  | And_refl of Scope.t * Imandrax_api_mir.Term.t
  | Or_false_left of Scope.t * Imandrax_api_mir.Term.t
  | Or_false_right of Scope.t * Imandrax_api_mir.Term.t
  | Or_true_left of Scope.t * Imandrax_api_mir.Term.t
  | Or_true_right of Scope.t * Imandrax_api_mir.Term.t
  | Or_refl of Scope.t * Imandrax_api_mir.Term.t
  | Imply_true_right of Scope.t * Imandrax_api_mir.Term.t
  | Imply_true_left of Scope.t * Imandrax_api_mir.Term.t
  | Imply_false_left of Scope.t * Imandrax_api_mir.Term.t
  | Imply_false_right of Scope.t * Imandrax_api_mir.Term.t
  | Imply_refl of Scope.t * Imandrax_api_mir.Term.t
  | Neq of Scope.t * Imandrax_api_mir.Term.t
  | Eq_const of Scope.t * Imandrax_api_mir.Term.t * Imandrax_api_mir.Term.t
  | Double_neg_elim of Scope.t * Imandrax_api_mir.Term.t
  | Eq_true_elim of Scope.t * Imandrax_api_mir.Term.t
  | Eq_false_not of Scope.t * Imandrax_api_mir.Term.t
  | Cut of Scope.t * proof_step offset_for * proof_step offset_for list
  | Subst of Scope.t * proof_step offset_for * (Imandrax_api_mir.Var.t * Imandrax_api_mir.Term.t) list

(** A proof step at the level of deep sequents. *)
and deep_proof_step =
  | Deep_cut of Scope.t * deep_proof_step offset_for * deep_proof_step offset_for list
  | Deep_intro of Scope.t * Scope.t * proof_step offset_for
  | Deep_subst of Scope.t * deep_proof_step offset_for * (Imandrax_api_mir.Var.t * Imandrax_api_mir.Term.t) list

(** A node in the proof tree, annotated with a deep sequent, used to encode the structure of the proof. *)
and deep_proof_tree =
  | Pt_root
  | Pt_node of deep_proof_tree offset_for * deep_proof_step offset_for
[@@deriving eq, twine, show, typereg]

[c-cube]

We'll merge this once it's used in imandrax!