SimplifiedExample.v

From Coq Require Import Program.Basics.
From Coq Require        Program.Equality.
From Coq Require Import Vectors.Vector.
From Coq Require Import Logic.Eqdep.

Import VectorNotations.

Require Import Lia.
Require Import ZArith.
Require Import ZifyBool.
Import ZifyClasses.

Definition Vec (n : nat) (a : Type) : Type := VectorDef.t a n.
Notation bitvector n := (Vec n bool).

(* Workaround for https://github.com/coq/coq/issues/16803 *)
Constraint Vec.u1 <= mkapp2.u0.
Constraint Vec.u1 <= mkapp2.u1.
Constraint Vec.u1 <= mkapp2.u2.
Constraint Vec.u1 <= mkrel.u0.
Constraint Vec.u1 <= mkapp.u0.
Constraint Vec.u1 <= mkapp.u1.

(* The exact definitions here aren't terribly important, so I've omitted them
   here for the sake of making this test case more minimal. *)
Definition bvToInt : forall w, bitvector w -> Z. Admitted.
Definition isBvult : forall w, bitvector w -> bitvector w -> Prop. Admitted.
Definition bvAdd : forall w, bitvector w -> bitvector w -> bitvector w. Admitted.

Definition bitvector_64 := bitvector 64.

(* Working *)
(*
Notation modulus := (Z.pow 2 64).
*)

(* Not working *)
Notation modulus := (Z.pow 2 (Z.of_nat 64)).

Global Program Instance Inj_bv_Z : InjTyp bitvector_64 Z :=
  { inj := bvToInt 64
  ; pred := fun x => Z.le 0 x /\ Z.lt x modulus
  }.
Next Obligation.
Admitted.

Global Program Instance Rel_eq_bv : BinRel (@eq bitvector_64) :=
  { TR := @eq Z
  }.
Next Obligation.
Admitted.

Global Program Instance Rel_isBvult : BinRel (isBvult 64 : bitvector_64 -> bitvector_64 -> Prop) :=
  { TR := Z.lt
  }.
Next Obligation.
Admitted.

Global Program Instance Op_bvAdd : BinOp (bvAdd 64 : bitvector_64 -> bitvector_64 -> bitvector_64) :=
  { TBOp := fun x y => Z.modulo (Z.add x y) modulus
  }.
Next Obligation.
Admitted.

Add Zify InjTyp Inj_bv_Z.
Add Zify BinRel Rel_eq_bv.
Add Zify BinRel Rel_isBvult.
Add Zify BinOp Op_bvAdd.

Ltac Zify.zify_convert_to_euclidean_division_equations_flag ::= constr:(true).

Lemma test_refl :
  forall (x : bitvector 64), x = x.
Proof. lia. Qed.

Lemma test_isBvult_trans :
  forall (x y z : bitvector 64),
  isBvult 64 x y -> isBvult 64 y z -> isBvult 64 x z.
Proof. lia. Qed.

Lemma test_bvAdd_comm :
  forall (x y : bitvector 64),
  bvAdd 64 x y = bvAdd 64 y x.
Proof. lia. Qed.

End S.

ZifyTermTakeTwo.v

From Coq Require Import Program.Basics.
From Coq Require        Program.Equality.
From Coq Require Import Vectors.Vector.
From Coq Require Import Logic.Eqdep.

Import VectorNotations.

Require Import Lia.
Require Import ZArith.
Require Import ZifyBool.
Import ZifyClasses.

Definition Vec (n : nat) (a : Type) : Type := VectorDef.t a n.
Notation bitvector n := (Vec n bool).

(* Workaround for https://github.com/coq/coq/issues/16803 *)
Constraint Vec.u1 <= mkapp2.u0.
Constraint Vec.u1 <= mkapp2.u1.
Constraint Vec.u1 <= mkapp2.u2.
Constraint Vec.u1 <= mkrel.u0.
Constraint Vec.u1 <= mkapp.u0.
Constraint Vec.u1 <= mkapp.u1.

(* The exact definitions here aren't terribly important, so I've omitted them
   here for the sake of making this test case more minimal. *)
Definition bvToInt : forall w, bitvector w -> Z. Admitted.
Definition isBvult : forall w, bitvector w -> bitvector w -> Prop. Admitted.
Definition bvAdd : forall w, bitvector w -> bitvector w -> bitvector w. Admitted.

Notation modulus w :=
  (Z.pow 2 (Z.of_nat w)).

Global Program Instance Inj_bv_Z w : InjTyp (bitvector w) Z :=
  { inj := bvToInt w
  ; pred := fun x => Z.le 0 x /\ Z.lt x (modulus w)
  }.
Next Obligation.
Admitted.

Global Program Instance Rel_eq_bv w : BinRel (@eq (bitvector w)) :=
  { TR := @eq Z
  }.
Next Obligation.
Admitted.

Global Program Instance Rel_isBvult w : BinRel (isBvult w) :=
  { TR := Z.lt
  }.
Next Obligation.
Admitted.

Global Program Instance Op_bvAdd w : BinOp (bvAdd w) :=
  { TBOp := fun x y => Z.modulo (Z.add x y) (modulus w)
  }.
Next Obligation.
Admitted.

Ltac Zify.zify_convert_to_euclidean_division_equations_flag ::= constr:(true).

Section S.

Variable w : nat.

Add Zify InjTyp (Inj_bv_Z w).
Add Zify BinRel (Rel_eq_bv w).
Add Zify BinRel (Rel_isBvult w).
Add Zify BinOp (Op_bvAdd w).

Lemma test_refl :
  forall (x : bitvector w), x = x.
Proof. lia. Qed.

Lemma test_isBvult_trans :
  forall (x y z : bitvector w),
  isBvult w x y -> isBvult w y z -> isBvult w x z.
Proof. lia. Qed.

Lemma test_bvAdd_comm :
  forall (x y : bitvector w),
  bvAdd w x y = bvAdd w y x.
Proof.
  (* Tactic failure:  Cannot find witness. *)
  Fail lia.
Admitted.

End S.