Proof by reflection in Coq

barendregt.v

From mathcomp
Require Import all_ssreflect.

Section Barendregt.

Variable P : Prop.

Fixpoint B (n : nat) := match n with | 1 => P | n'.+1 => P <-> B n' | 0 => False end.

Lemma B2n: forall n, n >= 1 -> B (2 * n).
Proof.
elim => //.
move => n IH Hlt.
rewrite mulnS /=.
case Hn: (2 * n); first by auto.
rewrite -Hn.
have Hlt': 0 < n by case: n IH Hlt Hn.
move/IH: Hlt' => Hlt'.
split => HP; first by split.
by apply HP.
Qed.

End Barendregt.

Lemma iffP : forall P : Prop, P <-> (P <-> (P <-> (P <-> (P <-> (P <-> (P <-> (P <-> (P <-> P)))))))).
Proof.
move => P.
set g := P <-> _.
have ->: g = B P 10 by [].
have ->: 10 = 2 * 5 by [].
exact: B2n.
Qed.