Library CFML.CFBuiltin

Set Implicit Arguments.
Require Import CFHeaps.
Require Export CFPrint.
Require Import LibInt LibString.

Generalizable Variables A.

Definition char := Ascii.ascii.

Definition array (A:Type) := loc.

Values that support polymorphic comparison

Axiom polymorphic_eq_arg : forall (A:Type), A -> Prop.

Axiom polymorphic_eq_arg_unit : forall (v:unit),
  polymorphic_eq_arg v.
Axiom polymorphic_eq_arg_int : forall (n:int),
  polymorphic_eq_arg n.
Axiom polymorphic_eq_arg_bool : forall (b:bool),
  polymorphic_eq_arg b.
Axiom polymorphic_eq_arg_char : forall (c:char),
  polymorphic_eq_arg c.
Axiom polymorphic_eq_arg_string : forall (s:string),
  polymorphic_eq_arg s.

Axiom polymorphic_eq_arg_none : forall A,
  polymorphic_eq_arg (@None A).
Axiom polymorphic_eq_arg_some : forall A (v:A),
  polymorphic_eq_arg v ->
  polymorphic_eq_arg (Some v).
Axiom polymorphic_eq_arg_nil : forall A,
  polymorphic_eq_arg (@nil A).
Axiom polymorphic_eq_arg_cons : forall A (v:A) (l:list A),
  polymorphic_eq_arg v ->
  polymorphic_eq_arg l ->
  polymorphic_eq_arg (v ::l).

Axiom polymorphic_eq_arg_tuple_2 :
  forall A1 A2 (v1:A1) (v2:A2),
  polymorphic_eq_arg v1 ->
  polymorphic_eq_arg v2 ->
  polymorphic_eq_arg (v1 ,v2 ).
Axiom polymorphic_eq_arg_tuple_3 :
  forall A1 A2 A3 (v1:A1) (v2:A2) (v3:A3),
  polymorphic_eq_arg v1 ->
  polymorphic_eq_arg v2 ->
  polymorphic_eq_arg v3 ->
  polymorphic_eq_arg (v1 ,v2 ,v3 ).
Axiom polymorphic_eq_arg_tuple_4 :
  forall A1 A2 A3 A4 (v1:A1) (v2:A2) (v3:A3) (v4:A4),
  polymorphic_eq_arg v1 ->
  polymorphic_eq_arg v2 ->
  polymorphic_eq_arg v3 ->
  polymorphic_eq_arg v4 ->
  polymorphic_eq_arg (v1 ,v2 ,v3 ,v4 ).
Axiom polymorphic_eq_arg_tuple_5 :
  forall A1 A2 A3 A4 A5 (v1:A1) (v2:A2) (v3:A3) (v4:A4) (v5:A5),
  polymorphic_eq_arg v1 ->
  polymorphic_eq_arg v2 ->
  polymorphic_eq_arg v3 ->
  polymorphic_eq_arg v4 ->
  polymorphic_eq_arg v5 ->
  polymorphic_eq_arg (v1 ,v2 ,v3 ,v4 ,v5 ).

Hint Resolve
  polymorphic_eq_arg_unit
  polymorphic_eq_arg_int
  polymorphic_eq_arg_bool
  polymorphic_eq_arg_char
  polymorphic_eq_arg_string
  polymorphic_eq_arg_none
  polymorphic_eq_arg_some
  polymorphic_eq_arg_nil
  polymorphic_eq_arg_cons
  polymorphic_eq_arg_tuple_2
  polymorphic_eq_arg_tuple_3
  polymorphic_eq_arg_tuple_4
  polymorphic_eq_arg_tuple_5
  : polymorphic_eq.

Tactic xpolymorphic_eq attempts to automatically solves goals of the form polymorphic_eq_arg v.

Do not use this tactic in the body of a Hint Extern, because it itself calls eauto.

Ltac xpolymorphic_eq_core tt :=
eauto with polymorphic_eq.

Tactic Notation "xpolymorphic_eq" :=
xpolymorphic_eq_core tt.

Pred / Succ

Definition pred (n:int) := (Coq.ZArith.BinInt.Z.sub n 1).

Definition succ (n:int) := (Coq.ZArith.BinInt.Z.add n 1).

Ignore

Definition ignore A (x:A) := tt.

Global Opaque
  Coq.ZArith.BinInt.Z.add
  Coq.ZArith.BinInt.Z.sub
  Coq.ZArith.BinInt.Z.mul
  Coq.ZArith.BinInt.Z.opp.

Global Transparent Coq.ZArith.BinInt.Z.sub.