🍃 Environment.v

Gitlab

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Export TezosOfOCaml.Proto_alpha.Environment_modules.
Require Export Lia.

Module Notations.
  Export Compare.Notations.
  Export Int32.Notations.
  Export Int64.Notations.
  Export Option.Notations.
  Export Pervasives.Notations.
  Export Z.Notations.
End Notations.
Export Notations.

Additional environment definitions, sometimes used by the tests.

Definition wrap_tzerror (error : Error_monad._error) : Error_monad._error :=
  error.

Definition wrap_tztrace t :=
  List.map wrap_tzerror t.

Definition wrap_tzresult {a : Set} (r : M? a) : M? a :=
  Result.map_error wrap_tztrace r.

Module Random.
  Module State.
    Parameter t : Set.

    Parameter make : array int → t.
  End State.
End Random.

Ltac Zify.zify_pre_hook ::=
  autounfold with tezos_z in *;
  unfold
    Pervasives.normalize_int,
    Pervasives.normalize_int32,
    Pervasives.normalize_int64 in *;
  unfold
    Pervasives.two_pow_31,
    Pervasives.two_pow_32,
    Pervasives.two_pow_62,
    Pervasives.two_pow_63,
    Pervasives.two_pow_64 in *;

  simpl (Compare.Int.(Compare.S.op_eq)) in *;
  simpl (Compare.Int.(Compare.S.op_ltgt)) in *;
  simpl (Compare.Int.(Compare.S.op_lt)) in *;
  simpl (Compare.Int.(Compare.S.op_gt)) in *;
  simpl (Compare.Int.(Compare.S.op_lteq)) in *;
  simpl (Compare.Int.(Compare.S.op_gteq)) in *;
  simpl (Compare.Int.(Compare.S.compare)) in *;
  simpl (Compare.Int.(Compare.S.max)) in *;
  simpl (Compare.Int.(Compare.S.min)) in *;
  simpl (Compare.Int.(Compare.S.equal)) in *;

  simpl (_ =i32 _) in *;
  simpl (_ ≠i32 _) in *;
  simpl (_ ≤i32 _) in *;
  simpl (_ <i32 _) in *;
  simpl (_ ≥i32 _) in *;
  simpl (_ >i32 _) in *;

  simpl (_ =i64 _) in *;
  simpl (_ ≠i64 _) in *;
  simpl (_ ≤i64 _) in *;
  simpl (_ <i64 _) in *;
  simpl (_ ≥i64 _) in *;
  simpl (_ >i64 _) in *;

  simpl (_ =Z _) in *;
  simpl (_ ≠Z _) in *;
  simpl (_ ≤Z _) in *;
  simpl (_ <Z _) in *;
  simpl (_ ≥Z _) in *;
  simpl (_ >Z _) in *;

  autounfold with tezos_z in *;
  trivial.

(* This is needed for lia work with rem and mod
   https://coq.inria.fr/refman/addendum/micromega.html#coq:tacn.zify *)
Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.

From Hammer Require Export Tactics.
From RecordUpdate Require Export RecordSet.

Parameter set_record_field : ∀ {A B : Set}, A → string → B → unit.

Parameter typ_with_with_non_trivial_matching : ∀ {A}, A.

Axioms and tactics about the existential casts generated by

coq-of-ocaml.

Axiom cast_exists_eval_1 :
  ∀ {T : Set → Set} {E1 : Set} {x : T E1},
  cast_exists T x = existT T E1 x.

Axiom cast_exists_eval_2 :
  ∀ {T : [Set ** Set] → Set} {E1 E2 : Set} {x : T [E1, E2]},
  cast_exists T x = existT T [E1, E2] x.

Axiom cast_exists_eval_3 :
  ∀ {T : [Set ** Set ** Set] → Set} {E1 E2 E3 : Set} {x : T [E1, E2, E3]},
  cast_exists T x = existT T [E1, E2, E3] x.

Axiom cast_exists_eval_4 :
  ∀ {T : [Set ** Set ** Set ** Set] → Set} {E1 E2 E3 E4 : Set}
    {x : T [E1, E2, E3, E4]},
  cast_exists T x = existT T [E1, E2, E3, E4] x.

Axiom cast_exists_eval_5 :
  ∀ {T : [Set ** Set ** Set ** Set ** Set] → Set} {E1 E2 E3 E4 E5 : Set}
    {x : T [E1, E2, E3, E4, E5]},
  cast_exists T x = existT T [E1, E2, E3, E4, E5] x.

Axiom cast_exists_eval_6 :
  ∀ {T : [Set ** Set ** Set ** Set ** Set ** Set] → Set}
    {E1 E2 E3 E4 E5 E6 : Set} {x : T [E1, E2, E3, E4, E5, E6]},
  cast_exists T x = existT T [E1, E2, E3, E4, E5, E6] x.

Ltac rewrite_cast_exists :=
  match goal with
  | |- context[cast_exists (Es := ?Es) ?T ?x] ⇒
    match Es with
    | Set ⇒ rewrite (cast_exists_eval_1 (T := T) (x := x))
    | [Set ** Set] ⇒ rewrite (cast_exists_eval_2 (T := T) (x := x))
    | [Set ** Set ** Set] ⇒ rewrite (cast_exists_eval_3 (T := T) (x := x))
    | [Set ** Set ** Set ** Set] ⇒
      rewrite (cast_exists_eval_4 (T := T) (x := x))
    | [Set ** Set ** Set ** Set ** Set] ⇒
      rewrite (cast_exists_eval_5 (T := T) (x := x))
    | [Set ** Set ** Set ** Set ** Set ** Set] ⇒
      rewrite (cast_exists_eval_6 (T := T) (x := x))
    end
  end.

Definition bind_prop {a trace : Set}
  (x : Pervasives.result a trace) (f : a → Prop) : Prop :=
  match x with
  | Pervasives.Ok x ⇒ f x
  | Pervasives.Error _ ⇒ True
  end.

Notation "'letP?' x ':=' X 'in' Y" :=
  (bind_prop X (fun x ⇒ Y))
  (at level 200, x name, X at level 100, Y at level 200).

Notation "'letP?' ' x ':=' X 'in' Y" :=
  (bind_prop X (fun x ⇒ Y))
  (at level 200, x pattern, X at level 100, Y at level 200).

Destruct the matched value in an expression [e].

Ltac destruct_match_in e :=
  lazymatch e with
  | context[match ?e with | _ ⇒ _ end] ⇒
    destruct_match_in e
  | context[let? _ := ?e in _] ⇒
    destruct_match_in e
  | _ ⇒ destruct e eqn:?
  end.

Destruct one matched value in the goal.

Ltac step :=
  match goal with
  | |- context[match ?e with | _ ⇒ _ end] ⇒
    destruct_match_in e
  | |- context[let? _ := ?e in _] ⇒
    destruct_match_in e
  end.

Document the proof state by requiring that a certain expression is there, either in the goal or the hypothesis.

Ltac grep e :=
  match goal with
  | |- context [e] ⇒ idtac
  | _ : context [e] |- _ ⇒ idtac
  | _ ⇒ fail "expression not found in the current goal"
  end.

Returns the head of a term, a helper used below

Ltac head f :=
  match f with
  | ?g _ ⇒ head g
  | _ ⇒ f
  end.

Unfolds [t] in [match t with ...] or [f] in [match f ... with ...

Ltac unfold_match :=
  match goal with
  | |- context [match ?e with _ ⇒ _ end] ⇒ let f := head e in unfold f
  end.

Destruct [e] in [if e ...]

Ltac step_outer_if :=
  match goal with
  | |- context [if ?e then _ else _] ⇒ destruct e eqn:?
  end.

Destruct [e] in [match e ...] (also works with [if e ...])

Ltac step_outer :=
  match goal with
  | |- context [match ?e with _ ⇒ _ end] ⇒ destruct e eqn:?
  end.

Tactic Notation "step_let?" := unfold op_gtgtquestion; step_outer; [|try easy].

Unfold [e] in [P e]

Ltac unfold_after H :=
  match goal with
  | |- H ?e ⇒ let e := head e in unfold e
  end.

Unfold [e] in [P _ e]

Ltac unfold_after1 H :=
  match goal with
  | |- H _ ?e ⇒ let e := head e in unfold e
  end.

Unfold [e] in [P _ _ e]

Ltac unfold_after2 H :=
  match goal with
  | |- H _ _ ?e ⇒ let e := head e in unfold e
  end.

Fails except if there are [n] subgoals remaining.

Tactic Notation "remaining_goals" integer(n) := let m := numgoals in guard n = m.

[ez t] is the same as [t; [simpl|easy..]]

Tactic Notation "ez" tactic(t) := t; [simpl|easy..].