jad-hamza

/** 
  * References:
  * https://github.com/FStarLang/FStar/blob/master/examples/paradoxes/berardi_minimal.fst
  * https://coq.inria.fr/library/Coq.Logic.Berardi.html
  * https://github.com/FStarLang/FStar/issues/360
  * Proof-irrelevance out of Excluded-middle and Choice in the Calculus of Constructions. 
  * F. Barbanera and S. Berardi. 1996.
  */

import stainless.lang._

jad-hamza

[Internal] Error: assertion failed. Trace:
[Internal] - scala.Predef$.assert(Predef.scala:156)
[Internal] - inox.ast.Paths$Path.withBound(Paths.scala:96)
[Internal] - inox.ast.Paths$Path.withBound(Paths.scala:76)
[Internal] - inox.ast.Paths$PathLike$$anonfun$withBounds$1.apply(Paths.scala:20)
[Internal] - inox.ast.Paths$PathLike$$anonfun$withBounds$1.apply(Paths.scala:20)
[Internal] - scala.collection.LinearSeqOptimized$class.foldLeft(LinearSeqOptimized.scala:124)
[Internal] - scala.collection.immutable.List.foldLeft(List.scala:84)
[Internal] - inox.ast.Paths$PathLike$class.withBounds(Paths.scala:20)
[Internal] - inox.ast.Paths$Path.withBounds(Paths.scala:76)

jad-hamza

Require Import Coq.Program.Tactics.

Program Definition g: {holds: bool | (holds = true)} := true.

Program Definition invoke2 (b: bool) (H: (match b with
                                          | true => g
                                          | false => true
                                          end = true)) : bool := true.

jad-hamza

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

jad-hamza

Require Import Coq.Program.Tactics.

Program Definition f: {holds: bool | (holds = true)} := true.

Program Definition g (b: bool) (H: (match b with
                                          | true => f
                                          | false => true
                                    end = true)) : bool := true.

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).

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

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.