Skip to content

Latest commit

 

History

History
73 lines (56 loc) · 2.84 KB

README.md

File metadata and controls

73 lines (56 loc) · 2.84 KB
Raw

STTfaXport

Copyright Deducteam [email protected] 2022

With STTfaXport, you can export theories written in Dedukti in the encoding of STTfa to other proof assistants.

To build STTfaXport, you need

  • OCaml (probably greater than 4.08)
  • Dedukti 2.7
  • dune

You are free to copy, modify or redistribute STTfaXport with attribution under the terms of the CeCILL-B license.

Install

$ dune install

Getting started

The following guide shows you how to export a single file to Coq.

  1. Download the file connectives.dk at https://raw.githubusercontent.com/Deducteam/sttfaxport/87442e6d81398a3dff18787a59ffa0bb38ebb39c/test/connectives.dk

  2. Download the encoding of STTfa https://raw.githubusercontent.com/Deducteam/sttfaxport/87442e6d81398a3dff18787a59ffa0bb38ebb39c/test/sttfa.dk

  3. Generate the object file of the encoding:

    dk check -e sttfa.dk

  4. Using a toplevel (ocaml or utop), print the translation of connectives.dk to Coq on the standard output:

    # #use "topfind";; (* Not necessary if you're using utop *)
# #require "sttfaxport";;
# Sttfaxport.(export Coq "connectives.dk")
Parameter True : Prop.
Parameter False : Prop.
Parameter Not : Prop -> Prop.
Parameter And : Prop -> Prop -> Prop.
Parameter Or : Prop -> Prop -> Prop.
Parameter ex : forall (A:Type), (A -> Prop) -> Prop.
Parameter equal : forall (A:Type), A -> A -> Prop.
Axiom I : True.
Axiom falsity : forall (t:Prop), False -> t.
Axiom nmk : forall (A:Prop), (A -> False) -> Not A.
Axiom Not_ind : forall (A:Prop), forall (Q:Prop), ((A -> False) -> Q) -> (Not A) -> Q.
Axiom conj : forall (A:Prop), forall (B:Prop), A -> B -> And A B.
Axiom match_And_prop : forall (A:Prop), forall (B:Prop), forall (return_:Prop), (A -> B -> return_) -> (And A B) -> return_.
Axiom or_introl : forall (A:Prop), forall (B:Prop), A -> Or A B.
Axiom or_intror : forall (A:Prop), forall (B:Prop), B -> Or A B.
Axiom match_Or_prop : forall (A:Prop), forall (B:Prop), forall (return_:Prop), (A -> return_) -> (B -> return_) -> (Or A B) -> return_.
Axiom ex_intro : forall A, forall (P:(A -> Prop)), forall (x:A), (P x) -> ex (A) P.
Axiom match_ex_prop : forall A, forall (P:(A -> Prop)), forall (return_:Prop), (forall (x:A), (P x) -> return_) -> (ex (A) P) -> return_.
Axiom refl_equal : forall A, forall (x:A), equal (A) x x.
Axiom equal_leibniz : forall A, forall (x:A), forall (y:A), (equal (A) x y) -> forall (P:(A -> Prop)), (P x) -> P y.
- : (unit, unit) result = Ok ()

What to do next

The file HACKING.md gives some instructions for developers.

You can report bugs on the issue tracker.

You can contact the developers at [email protected]