Commit 704d6d96 authored by Raphael Cauderlier's avatar Raphael Cauderlier
Browse files

Full Hol and Coq instantiation

parent 617567dc
......@@ -3,6 +3,7 @@ open "naturals";;
open "natural_zenon";;
open "natural_instantiation";;
open "natmorph";;
open "natural_full";;
(* Load HOL-Coq interoperability to make Coq types usable *)
type load_hol_to_coq =
......@@ -248,17 +249,17 @@ species CoqLe =
{* (n : hol.term abst_T => cbool_false). *};
end;;
(* species CoqMorph (B is NatPrimeDiv) = *)
(* inherit NatPrimeDivMorph(B), CoqLe, CoqTimes; *)
(* let morph(n) = coq_iter(n, B!zero, B!succ); *)
(* proof of morph_zero = *)
(* dedukti proof *)
(* definition of morph, zero *)
(* {* hol.REFL _p_B_T _p_B_zero. *}; *)
(* proof of morph_succ = *)
(* dedukti proof *)
(* definition of morph, succ *)
(* {* (n : (hol.term coq_nat__t) => *)
(* hol.REFL _p_B_T (abst_morph (abst_succ n))). *}; *)
(* end;; *)
species CoqMorph (B is NatPrimeDiv) =
inherit NatPrimeDivTransfer(B), CoqLe, CoqTimes;
let morph(n) = coq_iter(n, B!zero, B!succ);
proof of morph_zero =
dedukti proof
definition of morph, zero
{* hol.REFL _p_B_T _p_B_zero. *};
proof of morph_succ =
dedukti proof
definition of morph, succ
{* (n : (hol.term coq_nat__t) =>
hol.REFL _p_B_T (abst_morph (abst_succ n))). *};
end;;
open "basics";;
open "naturals";;
open "natural_zenon";;
open "natmorph";;
(* Extend the various MathTransfer hierarchies up to primality and the
prime divisor lemma *)
species NatDivides =
inherit NatTimes, NatLt;
logical let divides(m, n) = ex p : Self, times(m, p) = n;
theorem divides_times : all m n : Self,
divides(m, n) <-> (ex p : Self, times(m, p) = n)
proof = by definition of divides;
logical signature divides : Self -> Self -> prop;
property divides_times : all m n : Self,
divides(m, n) <-> (ex p : Self, times(m, p) = n);
end;;
species NatDividesZenon =
inherit NatDivides;
theorem divides_times_m : all m p : Self, divides(m, times(m, p))
......@@ -57,50 +59,44 @@ species NatDividesZenon =
<3>f conclude
<2>f conclude
<1>f conclude;
(* property divides_le : all m n : Self, *)
(* divides(m, n) -> *)
(* le(succ(succ(zero)), n) -> *)
(* le(m, n); *)
end;;
species NatStrictlyDivides =
inherit NatDivides, NatLt;
logical let sd(m, n) = divides(m, n) /\ lt(m, n) /\ lt(succ(zero), m);
theorem sd_divides : all m n : Self, sd(m, n) -> divides(m, n)
proof = by definition of sd;
theorem sd_lt : all m n : Self, sd(m, n) -> lt(m, n)
proof = by definition of sd;
theorem sd_1 : all m n : Self, sd(m, n) -> lt(succ(zero), m)
proof = by definition of sd;
theorem sd_intro : all m n : Self,
inherit NatDivides, NatLt, NatOne;
logical signature sd : Self -> Self -> prop;
property sd_divides : all m n : Self, sd(m, n) -> divides(m, n);
property sd_lt : all m n : Self, sd(m, n) -> lt(m, n);
property sd_1 : all m n : Self, sd(m, n) -> lt(one, m);
property sd_intro : all m n : Self,
divides(m, n) ->
lt(m, n) ->
lt(succ(zero), m) ->
sd(m, n)
proof = by definition of sd;
lt(one, m) ->
sd(m, n);
end;;
species NatPrime =
inherit NatStrictlyDivides;
logical let prime(p) = lt(succ(zero), p) /\ all d : Self, ~(sd(d, p));
theorem prime_1 : all p : Self, prime(p) -> lt(succ(zero), p)
proof = by definition of prime;
theorem prime_sd : all p d : Self, prime(p) -> ~(sd(d, p))
proof = by definition of prime;
theorem prime_intro :
inherit NatStrictlyDivides, NatOne;
logical signature prime : Self -> prop;
property prime_1 : all p : Self, prime(p) -> lt(one, p);
property prime_sd : all p d : Self, prime(p) -> ~(sd(d, p));
property prime_intro :
all p : Self,
lt(succ(zero), p) ->
lt(one, p) ->
(all d : Self, ~(sd(d, p))) ->
prime(p)
proof = by definition of prime;
prime(p);
end;;
species NatPrimeDiv =
inherit NatPrime, NatDividesZenon;
inherit NatPrime, NatDividesZenon, NatInd;
property divides_le : all m n : Self,
divides(m, n) ->
lt(one, n) ->
le(m, n);
property prime_divisor :
all n : Self,
(~(n = succ(zero))) ->
(~(n = one)) ->
ex p : Self, (prime(p) /\ divides(p, n));
signature primediv_pred : Self -> Self -> bool;
......@@ -117,10 +113,251 @@ species NatPrimeDiv =
<1>2 conclude;
theorem primediv_prime : all n : Self,
(~ n = succ(zero)) -> prime(primediv(n))
(~ n = one) -> prime(primediv(n))
proof = by property prime_divisor, choice_primediv, primediv_pred_spec;
theorem primediv_divides : all n : Self,
(~ n = succ(zero)) -> divides(primediv(n), n)
(~ n = one) -> divides(primediv(n), n)
proof = by property prime_divisor, choice_primediv, primediv_pred_spec;
end;;
species NatDividesInd = inherit NatDivides, NatInd; end;;
species NatDividesMorph(B is NatDividesInd) =
inherit NatDivides, NatTimesMorph(B), NatLtMorph(B);
theorem morph_divides :
all a1 a2 : Self,
divides(a1, a2) -> B!divides(morph(a1), morph(a2))
proof =
<1>1 assume a1 a2 : Self,
hypothesis H : divides(a1, a2),
prove B!divides(morph(a1), morph(a2))
<2>1 prove (ex a3 : Self, times(a1, a3) = a2)
by property divides_times hypothesis H
<2>2 prove (ex a3 : Self, morph(times(a1, a3)) = morph(a2))
by step <2>1
<2>3 prove (ex a3 : Self, B!times(morph(a1), morph(a3)) = morph(a2))
by step <2>2 property morph_times
<2>4 prove (ex b : B, B!times(morph(a1), b) = morph(a2))
by step <2>3
<2>5 prove B!divides(morph(a1), morph(a2))
by step <2>4 property B!divides_times
<2>f conclude
<1>2 conclude;
theorem morph_divides_rev :
all a1 a2 : Self,
B!divides(morph(a1), morph(a2)) -> divides(a1, a2)
proof =
<1>1 assume a1 a2 : Self,
hypothesis H : B!divides(morph(a1), morph(a2)),
prove divides(a1, a2)
<2>1 prove (ex b : B, B!times(morph(a1), b) = morph(a2))
by hypothesis H property B!divides_times
<2>2 prove (ex a3 : Self, B!times(morph(a1), morph(a3)) = morph(a2))
by step <2>1 property morph_surjective
<2>3 prove (ex a3 : Self, morph(times(a1, a3)) = morph(a2))
by step <2>2 property morph_times
<2>4 prove (ex a3 : Self, times(a1, a3) = a2)
<3>1 assume a3 : Self,
notation a = times(a1, a3),
hypothesis H1 : morph(times(a1, a3)) = morph(a2),
prove times(a1, a3) = a2
<4>1 prove morph(a) = morph(a2)
by hypothesis H1 definition of a
<4>2 prove morph(a) = morph(a2) -> a = a2
dedukti proof
property morph_injective
{* abst_morph_injective a a2 *}
<4>3 qed by step <4>1, <4>2 definition of a
<3>2 qed by step <3>1, <2>3
<2>f qed by step <2>4 property divides_times
<1>2 conclude;
end;;
species NatSDInd = inherit NatStrictlyDivides, NatInd; end;;
species NatSDMorph (B is NatSDInd) =
inherit NatStrictlyDivides, NatDividesMorph(B), NatLtMorph(B), NatOneMorph(B);
theorem morph_sd :
all a1 a2 : Self,
sd(a1, a2) -> B!sd(morph(a1), morph(a2))
proof =
<1>1 assume a1 a2 : Self,
hypothesis H : sd(a1, a2),
prove B!sd(morph(a1), morph(a2))
<2>1 prove divides(a1, a2)
by property sd_divides hypothesis H
<2>2 prove B!divides(morph(a1), morph(a2))
by property morph_divides step <2>1
<2>3 prove lt(a1, a2)
by property sd_lt hypothesis H
<2>4 prove B!lt(morph(a1), morph(a2))
by property morph_lt step <2>3
<2>5 prove lt(one, a1)
by property sd_1 hypothesis H
<2>6 prove B!lt(B!one, morph(a1))
by property morph_one, morph_lt step <2>5
<2>7 prove B!sd(morph(a1), morph(a2))
by property B!sd_intro
step <2>2, <2>4, <2>6
<2>f conclude
<1>f conclude;
theorem morph_sd_rev :
all a1 a2 : Self,
B!sd(morph(a1), morph(a2)) ->
sd(a1, a2)
proof =
<1>1 assume a1 a2 : Self,
hypothesis H: B!sd(morph(a1), morph(a2)),
prove sd(a1, a2)
<2>1 prove B!divides(morph(a1), morph(a2))
by property B!sd_divides hypothesis H
<2>2 prove divides(a1, a2)
by property morph_divides_rev step <2>1
<2>3 prove B!lt(morph(a1), morph(a2))
by property B!sd_lt hypothesis H
<2>4 prove lt(a1, a2)
by property morph_lt_rev step <2>3
<2>5 prove B!lt(B!one, morph(a1))
by property B!sd_1 hypothesis H
<2>6 prove B!lt(morph(one), morph(a1))
by property morph_one step <2>5
<2>7 prove lt(one, a1)
<3>1 prove B!lt(morph(one), morph(a1))
by step <2>6
<3>2 prove lt(one, a1)
by step <3>1 property morph_lt_rev
<3>f qed by step <3>2
<2>8 prove sd(a1, a2)
by property sd_intro
step <2>2, <2>4, <2>7
<2>f conclude
<1>f conclude;
end;;
species NatPrimeInd = inherit NatPrime, NatInd; end;;
species NatPrimeMorph (B is NatPrimeInd) =
inherit NatPrime, NatSDMorph(B), NatOneMorph(B);
theorem morph_prime : all p : Self, prime(p) -> B!prime(morph(p))
proof =
<1>1 assume p : Self,
hypothesis H : prime(p),
prove B!prime(morph(p))
<2>1 prove lt(one, p)
by property prime_1 hypothesis H
<2>2 prove B!lt(B!one, morph(p))
by property morph_lt, morph_one step <2>1
<2>3 prove (all d : Self, ~(sd(d, p)))
by property prime_sd hypothesis H
<2>4 prove (all d : B, ~(B!sd(d, morph(p))))
<3>1 assume d : B,
hypothesis Hd : B!sd(d, morph(p)),
prove false
<4>1 prove (ex a : Self, d = morph(a))
by property morph_surjective
<4>2 assume a : Self,
hypothesis Ha : d = morph(a),
prove false
<5>1 prove B!sd(morph(a), morph(p))
by hypothesis Hd, Ha
<5>2 prove sd(a, p)
by step <5>1 property morph_sd_rev
<5>3 qed by step <5>2
property prime_sd
hypothesis H
<4>f conclude
<3>3 conclude
<2>5 qed by step <2>2, <2>4 property B!prime_intro
<1>2 conclude;
theorem morph_prime_rev : all p : Self, B!prime(morph(p)) -> prime(p)
proof =
<1>1 assume p : Self,
hypothesis H : B!prime(morph(p)),
prove prime(p)
<2>1 prove B!lt(B!one, morph(p))
by property B!prime_1 hypothesis H
<2>2 prove lt(one, p)
by property morph_lt_rev, morph_one
step <2>1
<2>3 prove (all d : B, ~(B!sd(d, morph(p))))
by property B!prime_sd hypothesis H
<2>4 prove (all d : Self, ~(sd(d, p)))
<3>1 assume d : Self,
hypothesis Hd : sd(d, p),
prove false
<4>1 prove B!sd(morph(d), morph(p))
by property morph_sd hypothesis Hd
<4>f qed by step <4>1, <2>3
<3>3 conclude
<2>5 qed by step <2>2, <2>4 property prime_intro
<1>2 conclude;
end;;
species NatPrimeDivTransfer (B is NatPrimeDiv) =
inherit NatPrimeDiv, NatPrimeMorph(B);
proof of prime_divisor =
<1>1 assume n : Self,
hypothesis H : ~(n = one),
prove ex p : Self, (prime(p) /\ divides(p, n))
<2>1 hypothesis H2 : morph(n) = B!one,
prove false
<3>1 prove B!one = morph(one)
by property morph_one
<3>2 prove morph(n) = morph(one)
by hypothesis H2 step <3>1
<3>3 prove morph(n) = morph(one) -> (n = one)
by property morph_injective
<3>4 prove n = one
by step <3>2, <3>3
<3>f qed by step <3>4 hypothesis H
<2>2 prove ex p : B, (B!prime(p) /\ B!divides(p, morph(n)))
by step <2>1 property B!prime_divisor
<2>3 assume p : B,
hypothesis H2 : (B!prime(p) /\ B!divides(p, morph(n))),
assume p2 : Self,
hypothesis H3: p = morph(p2),
prove prime(p2) /\ divides(p2, n)
<3>1 prove B!prime(morph(p2))
by hypothesis H2, H3
<3>2 prove prime(p2)
by step <3>1 property morph_prime_rev
<3>3 prove B!divides(morph(p2), morph(n))
by hypothesis H2, H3
<3>4 prove divides(p2, n)
by step <3>3 property morph_divides_rev
<3>f conclude
<2>f qed by step <2>2, <2>3 property morph_surjective
<1>f conclude;
let primediv_pred(m, n) = B!primediv_pred(morph(m), morph(n));
proof of primediv_pred_spec =
<1>1 assume n p : Self,
prove (B!prime(morph(p)) /\ B!divides(morph(p), morph(n))) -> prime(p)
by property morph_prime_rev
<1>2 assume n p : Self,
prove (B!prime(morph(p)) /\ B!divides(morph(p), morph(n))) -> divides(p, n)
by property morph_divides_rev
<1>3 assume n p : Self,
prove (prime(p) /\ divides(p, n)) -> B!prime(morph(p))
by property morph_prime
<1>4 assume n p : Self,
prove (prime(p) /\ divides(p, n)) -> B!divides(morph(p), morph(n))
by property morph_divides
<1>f qed by step <1>1, <1>2, <1>3, <1>4
definition of primediv_pred
property B!primediv_pred_spec;
end;;
This diff is collapsed.
......@@ -3,6 +3,7 @@
(defun find-thm-number-in-buffer (statement)
"Find the theorem number corresponding to STATEMENT in the current buffer visiting HolNaturals.txt"
(goto-char (point-min))
(forward-line 1)
(while (not (eolp))
(search-forward (concat ": " statement)))
(beginning-of-line)
......
......@@ -12,9 +12,8 @@ end;;
species NatOne =
inherit NatDecl;
let one = succ(zero);
theorem one_spec : one = succ(zero)
proof = by definition of one;
signature one : Self;
property one_spec : one = succ(zero);
end;;
species NatBinary =
......@@ -54,10 +53,9 @@ end;;
species NatLe =
inherit NatPlus;
logical let le (m : Self, n : Self) = ex p : Self, plus(m, p) = n;
theorem le_plus : all m n : Self,
le(m, n) <-> (ex p : Self, plus(m, p) = n)
proof = by definition of le;
logical signature le : Self -> Self -> prop;
property le_plus : all m n : Self,
le(m, n) <-> (ex p : Self, plus(m, p) = n);
end;;
species NatMinus =
......@@ -71,9 +69,8 @@ end;;
species NatLt =
inherit NatLe;
logical let lt(m, n) = le(succ(m), n);
theorem lt_spec : all m n : Self, lt(m, n) <-> le(succ(m), n)
proof = by definition of lt;
logical signature lt : Self -> Self -> prop;
property lt_spec : all m n : Self, lt(m, n) <-> le(succ(m), n);
end;;
(* even, odd, factorial, pred, iter, pow, div, mod, bit0, bit1, distance, egcd, log, gcd, lcm, chineseRemainder *)
......@@ -126,6 +126,15 @@ species NatMorph (B is NatInd) =
<1>f conclude;
end;;
species NatOneInd = inherit NatOne, NatInd; end;;
species NatOneMorph (B is NatOneInd) =
inherit NatOne, NatMorph(B);
theorem morph_one : morph(one) = B!one
proof = by property one_spec, B!one_spec, morph_succ, morph_zero;
end;;
species NatPlusInd = inherit NatPlus, NatInd; end;;
species NatPlusMorph (B is NatPlusInd) =
......@@ -328,253 +337,3 @@ species NatLtMorph(B is NatLtInd) =
<2>f conclude
<1>2 conclude;
end;;
(* species NatDividesMorph(B is NatDivides) = *)
(* inherit NatDivides, NatTimesMorph(B), NatLtMorph(B); *)
(* theorem morph_divides : *)
(* all a1 a2 : Self, *)
(* divides(a1, a2) -> B!divides(morph(a1), morph(a2)) *)
(* proof = *)
(* <1>1 assume a1 a2 : Self, *)
(* hypothesis H : divides(a1, a2), *)
(* prove B!divides(morph(a1), morph(a2)) *)
(* <2>1 prove (ex a3 : Self, times(a1, a3) = a2) *)
(* by property divides_times hypothesis H *)
(* <2>2 prove (ex a3 : Self, morph(times(a1, a3)) = morph(a2)) *)
(* by step <2>1 *)
(* <2>3 prove (ex a3 : Self, B!times(morph(a1), morph(a3)) = morph(a2)) *)
(* by step <2>2 property morph_times *)
(* <2>4 prove (ex b : B, B!times(morph(a1), b) = morph(a2)) *)
(* by step <2>3 *)
(* <2>5 prove B!divides(morph(a1), morph(a2)) *)
(* by step <2>4 property B!divides_times *)
(* <2>f conclude *)
(* <1>2 conclude; *)
(* theorem morph_divides_rev : *)
(* all a1 a2 : Self, *)
(* B!divides(morph(a1), morph(a2)) -> divides(a1, a2) *)
(* proof = *)
(* <1>1 assume a1 a2 : Self, *)
(* hypothesis H : B!divides(morph(a1), morph(a2)), *)
(* prove divides(a1, a2) *)
(* <2>1 prove (ex b : B, B!times(morph(a1), b) = morph(a2)) *)
(* by hypothesis H property B!divides_times *)
(* <2>2 prove (ex a3 : Self, B!times(morph(a1), morph(a3)) = morph(a2)) *)
(* by step <2>1 property morph_surjective *)
(* <2>3 prove (ex a3 : Self, morph(times(a1, a3)) = morph(a2)) *)
(* by step <2>2 property morph_times *)
(* <2>4 prove (ex a3 : Self, times(a1, a3) = a2) *)
(* <3>1 assume a3 : Self, *)
(* notation a = times(a1, a3), *)
(* hypothesis H1 : morph(times(a1, a3)) = morph(a2), *)
(* prove times(a1, a3) = a2 *)
(* <4>1 prove morph(a) = morph(a2) *)
(* by hypothesis H1 definition of a *)
(* <4>2 prove morph(a) = morph(a2) -> a = a2 *)
(* dedukti proof *)
(* property morph_injective *)
(* {* abst_morph_injective a a2 *} *)
(* <4>3 qed by step <4>1, <4>2 definition of a *)
(* <3>2 qed by step <3>1, <2>3 *)
(* <2>f qed by step <2>4 property divides_times *)
(* <1>2 conclude; *)
(* (\* proof of divides_le = *\) *)
(* (\* <1>1 assume m n : Self, *\) *)
(* (\* hypothesis H1 : divides(m, n), *\) *)
(* (\* hypothesis H2 : le(succ(succ(zero)), n), *\) *)
(* (\* prove le(m, n) *\) *)
(* (\* <2>1 prove B!divides(morph(m), morph(n)) *\) *)
(* (\* by hypothesis H1 property morph_divides *\) *)
(* (\* <2>2 prove B!le(B!succ(B!succ(B!zero)), morph(n)) *\) *)
(* (\* by hypothesis H2 property morph_zero, morph_succ, morph_le *\) *)
(* (\* <2>3 prove B!le(morph(m), morph(n)) *\) *)
(* (\* by step <2>1, <2>2 property B!divides_le *\) *)
(* (\* <2>4 prove B!le(morph(m), morph(n)) -> le(m, n) *\) *)
(* (\* by property morph_le_rev *\) *)
(* (\* <2>f conclude *\) *)
(* (\* <1>f conclude; *\) *)
(* end;; *)
(* species NatSDMorph (B is NatStrictlyDivides) = *)
(* inherit NatStrictlyDivides, NatDividesMorph(B), NatLtMorph(B); *)
(* theorem morph_sd : *)
(* all a1 a2 : Self, *)
(* sd(a1, a2) -> B!sd(morph(a1), morph(a2)) *)
(* proof = *)
(* <1>1 assume a1 a2 : Self, *)
(* hypothesis H : sd(a1, a2), *)
(* prove B!sd(morph(a1), morph(a2)) *)
(* <2>1 prove divides(a1, a2) *)
(* by property sd_divides hypothesis H *)
(* <2>2 prove B!divides(morph(a1), morph(a2)) *)
(* by property morph_divides step <2>1 *)
(* <2>3 prove lt(a1, a2) *)
(* by property sd_lt hypothesis H *)
(* <2>4 prove B!lt(morph(a1), morph(a2)) *)
(* by property morph_lt step <2>3 *)
(* <2>5 prove lt(succ(zero), a1) *)
(* by property sd_1 hypothesis H *)
(* <2>6 prove B!lt(B!succ(B!zero), morph(a1)) *)
(* by property morph_succ, morph_zero, morph_lt *)
(* step <2>5 *)
(* <2>7 prove B!sd(morph(a1), morph(a2)) *)
(* by property B!sd_intro *)
(* step <2>2, <2>4, <2>6 *)
(* <2>f conclude *)
(* <1>f conclude; *)
(* theorem morph_sd_rev : *)
(* all a1 a2 : Self, *)
(* B!sd(morph(a1), morph(a2)) -> *)
(* sd(a1, a2) *)
(* proof = *)
(* <1>1 assume a1 a2 : Self, *)
(* hypothesis H: B!sd(morph(a1), morph(a2)), *)
(* prove sd(a1, a2) *)
(* <2>1 prove B!divides(morph(a1), morph(a2)) *)
(* by property B!sd_divides hypothesis H *)
(* <2>2 prove divides(a1, a2) *)
(* by property morph_divides_rev step <2>1 *)
(* <2>3 prove B!lt(morph(a1), morph(a2)) *)
(* by property B!sd_lt hypothesis H *)
(* <2>4 prove lt(a1, a2) *)
(* by property morph_lt_rev step <2>3 *)
(* <2>5 prove B!lt(B!succ(B!zero), morph(a1)) *)
(* by property B!sd_1 hypothesis H *)
(* <2>6 prove B!lt(morph(succ(zero)), morph(a1)) *)
(* by property morph_succ, morph_zero step <2>5 *)
(* <2>7 notation a = succ(zero), *)
(* prove lt(succ(zero), a1) *)
(* <3>1 prove B!lt(morph(a), morph(a1)) *)
(* by step <2>6 definition of a *)
(* <3>2 prove lt(a, a1) *)
(* by step <3>1 property morph_lt_rev *)
(* <3>f qed by step <3>2 definition of a *)
(* <2>8 prove sd(a1, a2) *)
(* by property sd_intro *)
(* step <2>2, <2>4, <2>7 *)
(* <2>f conclude *)
(* <1>f conclude; *)
(* end;; *)
(* species NatPrimeMorph (B is NatPrime) = *)
(* inherit NatPrime, NatSDMorph(B); *)
(* theorem morph_prime : all p : Self, prime(p) -> B!prime(morph(p)) *)
(* proof = *)
(* <1>1 assume p : Self, *)
(* hypothesis H : prime(p), *)
(* prove B!prime(morph(p)) *)
(* <2>1 prove lt(succ(zero), p) *)
(* by property prime_1 hypothesis H *)
(* <2>2 prove B!lt(B!succ(B!zero), morph(p)) *)
(* by property morph_lt, morph_succ, morph_zero step <2>1 *)
(* <2>3 prove (all d : Self, ~(sd(d, p))) *)
(* by property prime_sd hypothesis H *)
(* <2>4 prove (all d : B, ~(B!sd(d, morph(p)))) *)
(* <3>1 assume d : B, *)
(* hypothesis Hd : B!sd(d, morph(p)), *)
(* prove false *)
(* <4>1 prove (ex a : Self, d = morph(a)) *)
(* by property morph_surjective *)
(* <4>2 assume a : Self, *)
(* hypothesis Ha : d = morph(a), *)
(* prove false *)
(* <5>1 prove B!sd(morph(a), morph(p)) *)
(* by hypothesis Hd, Ha *)
(* <5>2 prove sd(a, p) *)
(* by step <5>1 property morph_sd_rev *)
(* <5>3 qed by step <5>2 *)
(* property prime_sd *)
(* hypothesis H *)
(* <4>f conclude *)
(* <3>3 conclude *)
(* <2>5 qed by step <2>2, <2>4 property B!prime_intro *)
(* <1>2 conclude; *)
(* theorem morph_prime_rev : all p : Self, B!prime(morph(p)) -> prime(p) *)
(* proof = *)
(* <1>1 assume p : Self, *)
(* hypothesis H : B!prime(morph(p)), *)
(* prove prime(p) *)
(* <2>1 prove B!lt(B!succ(B!zero), morph(p)) *)
(* by property B!prime_1 hypothesis H *)
(* <2>2 prove lt(succ(zero), p) *)
(* by property morph_lt_rev, morph_succ, morph_zero *)
(* step <2>1 *)