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.

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.