Library BoundedNat.looping_absurd

An inhabitant of any type in Type can be derived from False

without False_rect
without loop at extraction

Trick invented with Dominique Larchey-Wendling, presented in our chapter "The Braga method".

This results in alternatives to False_rec without Prop-to-Type leakage, including Fexc which is extracted as assert false.

Nothing new here (wrt. "The Braga method"), but used in other files of this directory.

From Stdlib Require Import Extraction.

Definition T := True.
Definition F := False.

Section sec_absurd.
Variable X : Type.
Variable f: F.

An arbitrary inductive proposition

  Definition P: Prop := T.

  Let Fixpoint loop (x:P) : X := loop (match f with end).

  Hypothesis p: P.
  Definition Floop_P : X := loop p.
End sec_absurd.

Definition Floop_T (X: Type) (f: F) : X :=
  (fix loop (_:T) := loop (match f with end)) I.
Definition Floop_F (X: Type) : F → X :=
  (fix loop f := loop (match f with end)).
Definition Floop (X: Type) : F → X :=
  (fix loop t (f:F) := loop tt (match f with end)) tt.
Definition Fexc {X: Type} (f: F) : X :=
  match Floop Empty_set f with end.
Extraction Fexc.