jad-hamza

trait A {
  var u: BigInt
  var v: BigInt
  def f(x: BigInt): BigInt
}

case class B(a: A)

object Example {
  def invariant(b: B) = {

jad-hamza

Require Import Coq.Program.Tactics.
Require Import Coq.Program.Program.
Require Import Omega.

Open Scope bool_scope.
Open Scope Z_scope.

Definition myMatch b A (e1: b = true -> A) (e2: b = false -> A): A.                    
  destruct b.
  - apply e1. reflexivity.

jad-hamza

def g(i) {
    require(i > 0)
    i >= -1
} ensuring(res => res)

def f(i): bool {
    require(i >= 0)
    i > 0
}

jad-hamza

Require Import Coq.Program.Tactics.
Require Import Coq.Program.Program.
Require Import Omega.

Open Scope bool_scope.
Open Scope Z_scope.

Program Definition g (i: Z) (h: (Z.gtb i 0 = true)) : {holds: bool | (holds = true)} :=
  Z.geb i (-1).
Next Obligation.

jad-hamza

Require Import Coq.Program.Tactics.
Require Import Coq.Program.Program.
Require Import Omega.

Open Scope bool_scope.
Open Scope Z_scope.

Program Definition g (i: Z) (h: (Z.gtb i 0 = true)) : {holds: bool | (holds = true)} :=
  Z.geb i (-1).

jad-hamza

Lemma dep_match: forall P b (e1: P true) (e2: P false) x,
    match b as y return P y with
    | true => e1
    | false => e2
    end = x ->
    (b = true /\ e1 = x) \/
    (b = false /\ e2 = x).
Admitted.
  

jad-hamza

Require Import Coq.Program.Tactics.
Require Import Coq.Program.Program.
Require Import Omega.

Open Scope bool_scope.
Open Scope Z_scope.

Program Definition g (i: Z) (h: (Z.gtb i 0 = true)) : {holds: bool | (holds = true)} :=
  Z.geb i (-1).

jad-hamza

Error: Abstracting over the term "b" leads to a term
fun b0 : bool =>
(i >? 0) = b0 ->
(if b0 as res0 return (res0 = b0 -> bool)
 then fun H : true = b0 => f (i - 1) (h_obligation_1 i H)
 else fun _ : false = b0 => false) eq_refl = true -> 
(i + 1 >? 0) = true
which is ill-typed.
Reason is: Illegal application: 
The term "h_obligation_1" of type

jad-hamza

Require Import Coq.Program.Tactics.
Require Import Coq.Program.Program.
Require Import Omega.

Open Scope bool_scope.
Open Scope Z_scope.

Program Definition g (i: Z) (h: (Z.gtb i 0 = true)) : {holds: bool | (holds = true)} :=
  Z.geb i (-1).

jad-hamza

Require Import Coq.Program.Tactics.
Require Import Coq.Program.Program.
Require Import Omega.

Open Scope bool_scope.
Open Scope Z_scope.

Program Definition g (i: Z) (h: (Z.gtb i 0 = true)) : {holds: bool | (holds = true)} :=
  Z.geb i (-1).