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

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

[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

/** 
  * 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._