Commit f8d4419a authored by Raphael Cauderlier's avatar Raphael Cauderlier
Browse files

Initial commit.

The FoCaLiZe development is taken from the work on interoperability
between Coq and HOL used to prove the sieve of Eratosthenes.
parents
.config_vars
.bkp/
*.dko
*.fo
*.pfc
*.zv
# Copyright Raphaël Cauderlier <raphael.cauderlier@irif.fr>, 2017
#
# This software is governed by the CeCILL-B license under French law and
# abiding by the rules of distribution of free software.
#
# See "http://www.cecill.info".
-include .config_vars
.config_vars: configure
./configure
SUBDIRS = core interop
all:
for d in $(SUBDIRS); do \
$(MAKE) all -C $$d; \
done
clean:
for d in $(SUBDIRS); do \
$(MAKE) clean -C $$d; \
done
install:
for d in $(SUBDIRS); do \
$(MAKE) install -C $$d; \
done
uninstall:
for d in $(SUBDIRS); do \
$(MAKE) uninstall -C $$d; \
done
.PHONY: all clean install uninstall
#+Title: MathTransfer: Transfer Theorems on Mathematical Structures
#+LaTeX_header: \newcommand[1]{\Cite{#1}}{~\cite{#1}}
* General Presentation of the MathTransfer library
If $A$ and $B$ are two isomorphic mathematical structures, then for
any formula $\varphi_A$ expressed in the language of $A$, the formula
$\varphi_A \to \varphi_B$ is a theorem where $\varphi_B$ is the
formula corresponding to $\varphi_A$ in the language of $B$.
Theorems of the form $\varphi_A \to \varphi_B$ are called transfer
theorems. The use of transfer theorems is a way to formalize
rigorously the mathematical habit of "reasoning modulo isomorphism".
Techniques for automatically proving transfer theorems in proof
assistants have been proposed in Isabelle/HOL\Cite{IsabelleTransfer}
and more recently in Coq\Cite{CoqTransfer} but to our knowledge, no
formal library of mathematical structures and proofs of transfer
theorems has yet been proposed.
An interesting application of transfer is interoperability of proof
systems. Interoperability can be decomposed in two major steps:
1) translating each proof system that we are willing to interoperate
into a common formalism
2) proving transfer theorems in this common formalism to relate the
separately translated developments
As common formalism in the first step, we use the Dedukti logical
framework\Cite{Dedukti} for which translators from a large variety of
proof systems have been developed.
MathTransfer is composed of a core aiming at solving the second step
and an interoperability library built on top of the core and
consisting in arithmetic and algebraic results imported from various
proof assistants.
The core of the MathTransfer library consists in formal proofs of
transfer theorems for a variety of mathematical structures coming from
arithmetic and algebra. It is written in FoCaLiZe\Cite{focalize}, a
language that eases the definition of mathematical structures and the
automation of proofs and for which a translator to Dedukti exists.
* Content of the MathTransfer library
** Core
The core of the MathTransfer library, located in the [[./core][core]] directory
defines arithmetic and algebraic structures and the morphisms between
such structures but does not contain any interesting properties of
these structures. For example, the structure of natural numbers with
addition is defined in the file [[./core/arith/naturals.fcl][core/arith/naturals.fcl]] but it does
not contain proofs for the associativity and commutativity of addition
because these properties are not helpful for proving transfer
theorems. They can however be imported from any arithmetic library so
they are proved in the interoperability library.
*** Logic
The logic used in the MathTransfer library is an higher-order logic
seen as an extension of multi-sorted first-order logic.
**** TODO detail the description of the logic
*** Arithmetic
The directory [[./core/arith][core/arith]] contains the definitions of arithmetical
structures, that is mathematical structures about natural numbers and
integers.
**** Natural numbers
The file [[./core/arith/naturals.fcl][core/arith/naturals.fcl]] defines the following species
representing mathematical structures built from natural numbers with
various operations and relations:
- Peano axioms
Peano axiomatization of natural numbers forms the first building
block of the arithmetic library: the =NatDecl= species in file
=naturals.fcl=. This species requires two functions: =zero= of type
=Self= and =succ= of type =Self -> Self= and three axioms:
=zero_succ= expressing that =zero= is the successor of no natural
number, =succ_inj= expressing the injectivity of =succ= and =ind=
expressing the induction axiom. We see =ind= as a single
first-order axiom by representing predicate (and function)
application as a binary operation =@=.
- Reasoning by case (all numbers are zero or successors)
In FoCaLiZe, first-order statements are easier to use than
higher-order ones because the first-order theorem prover Zenon can
assist the user in the first case and not in the second case.
An inductive argument that does not actually use the induction
hypothesis is the same thing than reasoning by case on a natural
number and this can be stated as a first-order theorem: any natural
number is either zero or the successor of some natural number.
- Addition
=plus= is a binary operation over natural numbers defined by the
following axioms:
+ =plus(zero, n) = n=
+ =plus(succ(m), n) = succ(plus(m, n))=
- Multiplication
=times= is a binary operation over natural numbers defined by the
following axioms:
+ =times(zero, n) = zero=
+ =times(succ(m), n) = plus(n, times(m, n))=
- Ordering
=le= is a binary relation over natural numbers defined by the following axiom:
+ =le(m, n) <-> (ex p : Self, plus(m, p) = n)=
- Subtraction
=minus= is a binary operation over natural numbers defined by the
following axioms:
+ =minus(zero, n) = zero=
+ =minus(succ(n), zero) = succ(n)=
+ =minus(succ(m), succ(n)) = minus(m, n)=
- Strict ordering
=lt= is a binary relation over natural numbers defined by the following axiom:
+ =lt(m, n) <-> le(succ(m), n)=
- Divisibility
=divides= is a binary relation over natural numbers defined by the following axiom:
+ =divides(m, n) <-> (ex p : Self, times(m, p) = n)=
- Strict Divisibility
=sd= is a binary relation over natural numbers defined by the following axiom:
+ =sd(m, n) <-> (divides(m, n) /\ lt(m, n) /\ lt(succ(zero), m))=
- Primality
=prime= is a predicate over natural numbers defined by the following axiom:
+ =prime(p) <-> lt(succ(zero), p) /\ all d : Self, ~(sd(d, p))=
**** TODO Integers
*** TODO Algebra
* TODO Related work
** Automating proofs of transfer theorems
*** In Isabelle/HOL
*** In Coq
*** In Dedukti
** TODO Proof reuse
Nicolas Magaud
Planning?
** TODO Univalent foundations
Ongoing program of founding mathematics on type theory using the
univalent axiom. This work does not assume an extra axiom. Can be
related to computational content of univalence.
* Future work
Better distinction between bool and Prop: because of the use of
OpenTheory stdlib, we tend to confuse bool and Prop. Decidable
operations on natural numbers should be in bool.
Setoids: The development would be a bit more general if it did not
depend on equality. This would make the library more compatible with
FoCaLiZe stdlib.
#! /bin/bash
print_to_file ()
{
echo "$1" >> .config_vars
}
print_to_stderr ()
{
echo "$1" > /dev/stderr
}
find_binary () {
# $1 is the name of the binary
# $2 is an optional extension to be used when we fallback to using
# locate
# Start by looking in path
print_to_stderr "Looking for program '$1' in PATH"
A=$(which "$1")
if [ -n "$A" ]
then
print_to_stderr "program '$1' found in PATH at \"$A\""
echo "$A"
return 0
# else use locate
else
print_to_stderr "program '$1' not found in PATH, trying with locate"
A=$(locate "$1$2" | head -n 1)
if [ -n "$A" ]
then
print_to_stderr "program '$1$2' found using locate at \"$A\""
echo "$A"
return 0
else
print_to_stderr "program '$1$2' not found"
return 1
fi
fi
}
find_binary_no_check () {
# $1 and $2 are arguments to find_binary
# $3 is the variable name
A=$(find_binary $1 $2)
print_to_file "$3=\"$A\""
return 0
}
find_and_check_binary () {
# $1 and $2 are arguments to find_binary
# $3 is the variable name
# $4 is the option to pass to the program to ask for its version
# $5 is the expected answer
A=$(find_binary $1 $2)
print_to_stderr "asking '$1' for its version number"
B=$($A $4 |& cat)
print_to_stderr "'$1' has version '$B'"
if [ "$B" = "$5" ]
then
print_to_stderr "'$1' has the expected version number"
print_to_file "$3=\"$A\""
return 0
else
print_to_stderr "'$1' has version '$B' but version '$5' was expected"
return 1
fi
}
echo > .config_vars &&
# Mandatory
find_binary_no_check "dkdep" ".native" "DKDEP" &&
find_and_check_binary "dkcheck" ".native" "DKCHECK" "-version" "Dedukti v2.5.1" &&
find_and_check_binary "dkmeta" ".native" "DKMETA" "-version" "Meta Dedukti v2.5.1" &&
find_and_check_binary "skcheck" ".native" "SKCHECK" "-version" "Sukerujo v2.5.1" &&
find_and_check_binary "skmeta" ".native" "SKMETA" "-version" "Meta Sukerujo v2.5.1" &&
find_and_check_binary "focalizec" "" "FOCALIZEC" "-v" "The FoCaLize compiler, version 0.9.2" &&
find_binary_no_check "dktactics" "" "DKTACTICS"
SUBDIRS = logic arith algebra
all:
for d in $(SUBDIRS); do \
$(MAKE) all -C $$d; \
done
clean:
for d in $(SUBDIRS); do \
$(MAKE) clean -C $$d; \
done
install:
for d in $(SUBDIRS); do \
$(MAKE) install -C $$d; \
done
uninstall:
for d in $(SUBDIRS); do \
$(MAKE) uninstall -C $$d; \
done
.PHONY: all clean install uninstall
include ../../.config_vars
.SUFFIXES: .dk .dko .sk .fcl
.SECONDARY:
all: natmorph.dko
INCLUDE_DIRS= -I ../logic
DKTACTICS_DIR=$(shell $(DKTACTICS))
DKCHECK_OPT = -I $(DKTACTICS_DIR)/fol $(INCLUDE_DIRS) -coc
FOCALIZEC_OPT = $(INCLUDE_DIRS) -no-ocaml-code -no-coq-code -stop-before-dk --experimental
.dk.dko:
$(DKCHECK) $(DKCHECK_OPT) -e -nl $<
.sk.dko:
$(SKCHECK) $(DKCHECK_OPT) -e -nl $<
.fcl.sk:
$(FOCALIZEC) $(FOCALIZEC_OPT) $<
naturals.dko : naturals.sk
natmorph.dko : natmorph.sk naturals.dko
natmorph.sk: naturals.dko
clean :
rm -f *.dko *.sk* *.fo *.pfc *.zv *.mangled *_fcl.*
This diff is collapsed.
(* An implementation of a hierarchy of representation of natural numbers *)
open "basics";;
(* Explicit application to help Zenon accept applied variables *)
let ( @ ) (f, x) = f(x);;
(* The basic block: Peano axiomatization of natural numbers *)
species NatDecl =
signature zero : Self;
signature succ : Self -> Self;
property zero_succ : all n : Self, ~(zero = succ(n));
property succ_inj : all m n : Self, succ(m) = succ(n) -> m = n;
property ind : all p : Self -> prop,
p @ zero ->
(all n : Self, p @ n -> p @ (succ(n))) ->
all n : Self, p @ n;
end;;
species NatCase =
inherit NatDecl;
(* When the induction hypothesis is not needed, we can use
reasoning by case which is better supported by Zenon *)
logical let casep (n : Self) = n = zero \/ ex m : Self, n = succ(m);
theorem case : all n : Self, n = zero \/ ex m : Self, n = succ(m)
proof =
<1>1 assume n : Self,
prove casep(n) <-> (n = zero \/ ex m : Self, n = succ(m))
by definition of casep
<1>2 prove casep(zero) ->
(all n : Self, casep(n) -> casep(succ(n))) ->
all n : Self, casep(n)
dedukti proof property ind {* abst_ind abst_casep *}
<1>3 prove casep(zero) by step <1>1
<1>4 assume n : Self, prove casep(succ(n)) by step <1>1
<1>f conclude;
end;;
species NatPlus =
inherit NatCase;
signature plus : Self -> Self -> Self;
property zero_plus : all n : Self, plus(zero, n) = n;
property succ_plus : all m n : Self, plus(succ(m), n) = succ(plus(m, n));
(* property plus_zero : all m : Self, plus(m, zero) = m; *)
end;;
species NatTimes =
inherit NatPlus;
signature times : Self -> Self -> Self;
property zero_times : all n : Self, times(zero, n) = zero;
property succ_times : all m n : Self, times(succ(m), n) = plus(n, times(m, n));
end;;
(* Ordering *)
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;
end;;
species NatMinus =
inherit NatPlus;
signature minus : Self -> Self -> Self;
property minus_zero_n : all n : Self, minus(zero, n) = zero;
property minus_succ_zero : all n : Self, minus(succ(n), zero) = succ(n);
property minus_succ_succ :
all m n : Self, minus(succ(m), succ(n)) = minus(m, n);
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;
end;;
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;
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,
divides(m, n) ->
lt(m, n) ->
lt(succ(zero), m) ->
sd(m, n)
proof = by definition of sd;
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 :
all p : Self,
lt(succ(zero), p) ->
(all d : Self, ~(sd(d, p))) ->
prime(p)
proof = by definition of prime;
end;;
(* species NatPrimeDiv = *)
(* inherit NatPrime; *)
(* property prime_divisor : *)
(* all n : Self, *)
(* (~(n = succ(zero))) -> *)
(* ex p : Self, (prime(p) /\ divides(p, n)); *)
(* signature primediv_pred : Self -> Self -> bool; *)
(* property primediv_pred_spec : all n p : Self, *)
(* primediv_pred(n, p) <-> (prime(p) /\ divides(p, n)); *)
(* let primediv (n : Self) : Self = select (primediv_pred(n)); *)
(* theorem choice_primediv : all n p : Self, *)
(* primediv_pred(n, p) -> primediv_pred(n, primediv(n)) *)
(* proof = *)
(* <1>1 assume n p : Self, *)
(* prove primediv_pred(n, p) -> primediv_pred(n, primediv(n)) *)
(* dedukti proof definition of primediv property choice *)
(* {* abst_choice (abst_primediv_pred n) p *} *)
(* <1>2 conclude; *)
(* theorem primediv_prime : all n : Self, *)
(* (~ n = succ(zero)) -> 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) *)
(* proof = by property prime_divisor, choice_primediv, primediv_pred_spec; *)
(* end;; *)
include ../../.config_vars
.SUFFIXES: .dk .dko .sk .fcl
.SECONDARY:
all: basics.dko zen.dko focal.dko
DKTACTICS_DIR=$(shell $(DKTACTICS))
DKCHECK_OPT = -I $(DKTACTICS_DIR)/fol -coc
FOCALIZEC_OPT = -no-ocaml-code -no-coq-code -stop-before-dk --experimental
.dk.dko:
$(DKCHECK) $(DKCHECK_OPT) -e -nl $<
.sk.dko:
$(SKCHECK) $(DKCHECK_OPT) -e -nl $<
.fcl.sk:
$(FOCALIZEC) $(FOCALIZEC_OPT) $<
basics.dko: dk_builtins.dko
cc.dko:
dk_bool.dko:
dk_logic.dko: cc.dko dk_bool.dko
focal.dko: dk_logic.dko dk_bool.dko zen.dko
basics.sk: basics.fcl dk_logic.dko dk_bool.dko
$(FOCALIZEC) $(FOCALIZEC_OPT) -no-stdlib-path $<
clean :
rm -f *.dko *.sk* *.fo *.pfc *.zv *.mangled *_fcl.* basics.dk
type bool = internal external | dedukti -> {*
dk_bool.bool.
def true := dk_bool.true.
def false := dk_bool.false
*};;
let ( = ) =
internal 'a -> 'a -> bool
external | dedukti -> {* dk_bool.eq __var_a *}
;;
let syntactic_equal = ( = );;
let ( <-> ) =
internal bool -> bool -> bool
external | dedukti -> {* _equal_ bool__t *}
;;
let ( ~~ ) =
internal bool -> bool
external | dedukti -> {* dk_bool.not *}
;;
let ( && ) =
internal bool -> bool -> bool
external | dedukti -> {* dk_bool.and *}
;;
let ( || ) =
internal bool -> bool -> bool
external | dedukti -> {* dk_bool.or *}
;;
let ( ==> ) =
internal bool -> bool -> bool
external | dedukti -> {* dk_bool.imp *}
;;
(* let ( ! ) = *)
(* internal ('a -> bool) -> bool *)
(* external | dedukti -> {* hol.forall __var_a *} *)
(* ;; *)
let cond (b, t, e) = if b then t else e;;
#NAME cc.
def eT := fol.term.
def Arrow : Type -> Type -> Type.
[A,B] Arrow A B --> fol.term A -> fol.term B.
#NAME dk_bool.
bool : Type.
def Bool : Type := bool.
def bool1 := fol.read_types (nat.S nat.O) bool.
IS_TRUE : fol.predicate.
[] fol.pred_arity IS_TRUE --> bool1.
def is_true : Bool -> fol.prop := fol.pred_apply IS_TRUE.
IS_FALSE : fol.predicate.
[] fol.pred_arity IS_FALSE --> bool1.
def is_false : Bool -> fol.prop := fol.pred_apply IS_FALSE.
TRUE : fol.function.
[] fol.fun_arity TRUE --> fol.nil_type.
[] fol.fun_codomain TRUE --> bool.
FALSE : fol.function.
[] fol.fun_arity FALSE --> fol.nil_type.
[] fol.fun_codomain FALSE --> bool.
def true : fol.term bool := fol.fun_apply TRUE.
def false : fol.term bool := fol.fun_apply FALSE.
EQ : A : Type -> fol.function.
[A] fol.fun_arity (EQ A) --> fol.read_types (nat.S (nat.S nat.O)) A A.
[] fol.fun_codomain (EQ _) --> bool.
def eq (A : Type) := fol.fun_apply (EQ A).
NOT : fol.function.
[] fol.fun_arity NOT --> fol.read_types (nat.S nat.O) bool.
[] fol.fun_codomain NOT --> bool.
def not := fol.fun_apply NOT.
def bool2 := fol.read_types (nat.S (nat.S nat.O)) bool bool.