Commit beecfe4a authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

19 dec

parent 851f7d80

Too many changes to show.

To preserve performance only 1000 of 1000+ files are displayed.

......@@ -9,6 +9,8 @@ verine/*
zenon_dk/*
focalide_dks/*
holide_lib/*
iProverModulo_dk/*
iProverModulo/*
dklib-master/*
TermChecker/*.txt
\ No newline at end of file
TermChecker/*.txt
temp/*
*.tmp
\ No newline at end of file
......@@ -4,4 +4,4 @@ A : Type.
f: A -> A -> A.
def g: A -> (A -> A).
[x] g x --> (y => f y x).
[x] g x --> (y : A => f y x).
......@@ -30,7 +30,7 @@ def and_ : n : Nat -> Bool_ n.
def and_ : n : Nat -> Bool_ n.
[] and_ 0 --> True.
[x] and_ (S 0) --> (x => x).
[] and_ (S 0) --> (x => x).
[n] and_ (S (S n)) --> (x : Bool => y : Bool => (and_ (S n) (and x y))).
(; ;)
......
......@@ -17,7 +17,7 @@ Snoc : list -> t -> list.
def expandn : n : nat -> lnt n -> list -> lnt n.
[l] expandn O (List O) l --> l
[n,l,l',a] expandn (S n) l l' --> a : t => expandn n (l a) (Snoc l' a).
[n,l,l'] expandn (S n) l l' --> a : t => expandn n (l a) (Snoc l' a).
a : t.
......
......@@ -119,7 +119,7 @@ def if : A : type -> (eps Bool) -> (eps A) -> (eps A) -> (eps A).
def leq : (eps Nat) -> (eps Nat) -> (eps Bool).
[] leq 0 _ --> True.
[x] leq (S _) 0 --> False.
[] leq (S _) 0 --> False.
[x,y] leq (S x) (S y) --> leq x y.
def for : A : type -> (eps A) -> (eps Nat) -> (eps Nat) -> ((eps Nat) -> (eps A) -> (eps A)) -> (eps A).
......
#NAME miller.
R : Type.
0 : R.
def p : R -> R -> R.
[x] p 0 x --> x.
[x] p x 0 --> x.
sh : R -> R.
ch : R -> R.
def d : (R -> R) -> (R -> R).
[] d sh --> ch.
[] d ch --> sh.
[] d (x => sh x) --> ch.
[] d (x => ch x) --> sh.
R2 : Type.
pair : R -> R -> R2.
def dx : (R -> R -> R) -> (R -> R -> R).
[F] dx (x => y => F x) --> x => y => (d (x => F x)) x.
[F] dx (x => y => F y) --> x => y => 0.
def dy : (R -> R -> R) -> (R -> R -> R).
[F] dy (x => y => F x) --> x => y => 0.
[F] dy (x => y => F y) --> x => y => (d (x => F x)) x.
def grad : (R -> R -> R) -> (R -> R -> R2).
[F] grad F --> x => y => pair ((dx F) x y) ((dy F) x y).
def plus : (R -> R -> R) -> (R -> R -> R) -> (R -> R -> R).
[F,G] plus F G --> (x => y => p (F x y) (G x y)).
[F,G] dx (x => y => p (F x y) (G x y)) -->
x => y => p ((dx (x => y => F x y)) x y)
((dx (x => y => G x y)) x y).
[F,G] dy (x => y => p (F x y) (G x y)) -->
x => y => p ((dy (x => y => F x y)) x y)
((dy (x => y => G x y)) x y).
def trans : (R -> R -> R) -> (R -> R -> R).
[F] trans F --> x => y => F y x.
def flip : (R -> R -> R2) -> (R -> R -> R2).
[F,G] flip (x => y => pair (F x y) (G x y)) --> x => y => pair (G x y) (F x y).
def f : R -> R -> R := plus (x : R => y : R => ch x) (x : R => y : R => sh y).
#SNF flip (grad f).
#NSTEPS #20 flip (grad f).
#SNF grad (trans f).
#CONV grad (trans f), flip (grad f).
......@@ -3,7 +3,7 @@ import sys
toStudy=open("erreur_"+sys.argv[1]+".txt",'r')
current=0
every=[[],[],[],[],[],[],[],[]]
every=[[],[],[],[],[]]
for line in toStudy:
if line.find("SUCCESS The file was proved terminating")==0:
current=0
......@@ -32,28 +32,28 @@ for line in toStudy:
elif line.find("ERROR There is a typing error")==0:
current=12
elif line.find("SUCCESS File")==0:
if current<7:
if current<4:
every[current].append(line.split("'")[1])
else:
every[7].append(line.split("'")[1])
every[4].append(line.split("'")[1])
else:
print(line)
toStudy.close()
longueur=0
for i in range(8):
for i in range(5):
a=len(every[i])
if a>longueur:
longueur=a
toFill=open("../../Bureau/TabRes.csv",sys.argv[2])
toFill.write(";;;"+sys.argv[1]+";;;;\n;;;;;;;;\n")
toFill.write("Accepted;Refused;Pattern Matching;Non-positive;Non linearity;Ext_rule;CompError;Autres\n")
toFill.write(";;"+sys.argv[1]+";;\n;;;;\n")
toFill.write("Accepted;Refused;Pattern Matching;Non-positive;Autres\n")
for i in range(longueur):
for j in range(8):
for j in range(5):
if len(every[j])>i:
toFill.write(every[j][i])
if j==7:
if j==4:
toFill.write('\n')
else:
toFill.write(";")
......
SHELL = /bin/bash
# The TPTP problems are in DIR/tptp, filtered problems and generated
# Dedukti files are in DIR/PDIR
PDIR = Problems
include config_vars
# The DIR/*_all files lists all solved problems, one per line.
# To count the solutions, we count the lines in these files
# This is used for informing the user of the progression in the
# benchmark and for the final statistics
NK_N = $(shell cat $(DIR)/nk_all | wc -l)
# The list of all files at step n+1 computed from the list of
# non-empty files at step n.
#
# The full picture:
# f.p -> f.filtered.p -> f.zen.dk -> f.ctx.dk
# L-> f.tab.dk -> f.nk.dk -> f.0.dk -> ... -> f.N.dk -> f.reduced.dk -> f.nj.dk
# | L-> f.still_classical.dk
# L-> f.zenonide_dk.dk -> f.zenonide_proof.dk
ALL_NJ = $(shell cat $(DIR)/nk_all | sed 's/\.nk\.dk/.nj.dk/')
all: $(ALL_NJ)
@echo $(ALL_NJ)
$(DIR)/%_all:
file $(DIR)/$(PDIR)/*.$*.dk | grep -v empty | cut -d ' ' -f 1 | sed 's/://' > $@
# Hand-written Dedukti files:
fo.dko: fo.dk
dkcheck -e $<
NJ.dko: NJ.dk fo.dko
dkcheck -e $<
classic/NK.dko: classic/NK.dk fo.dko NJ.dko
cd classic && dkcheck -e -I .. ../$<
classic/lem.dko: classic/lem.dk fo.dko NJ.dko classic/NK.dko
cd classic && dkcheck -e -I .. ../$<
classic/dn0.dko: classic/dn0.dk fo.dko NJ.dko classic/NK.dko
cd classic && dkcheck -e -I .. ../$<
classic/dn1.dko: classic/dn1.dk fo.dko NJ.dko classic/NK.dko
cd classic && dkcheck -e -nl -I .. ../$<
classic/dn2.dko: classic/dn2.dk fo.dko NJ.dko classic/NK.dko
cd classic && dkcheck -e -I .. ../$<
classic/dn3.dko: classic/dn3.dk fo.dko NJ.dko classic/NK.dko
cd classic && dkcheck -e -nl -I .. ../$<
classic/zen.dko: classic/zen.dk fo.dko NJ.dko classic/NK.dko
cd classic && dkcheck -e -I .. ../$<
intuitionistic/zen.dko: intuitionistic/zen.dk fo.dko NJ.dko
cd intuitionistic && dkcheck -e -I .. ../$<
# Reduce the natural deduction proof
$(DIR)/$(PDIR)/%.reduced.dk: $(DIR)/$(PDIR)/%.nk.dk $(DIR)/$(PDIR)/%.ctx.dk fo.dko NJ.dko classic/zen.dko classic/NK.dko classic/dn0.dko classic/dn1.dko classic/dn2.dko classic/dn3.dko classic/lem.dko $(DIR)/nk_all
@cat -n $(DIR)/nk_all | grep $<
@echo "/ $(NK_N)"
. reduce.sh && constructivize "$(DIR)/$(PDIR)/$*"
# Check it as a constructive proof
$(DIR)/$(PDIR)/%.nj.dk: $(DIR)/$(PDIR)/%.reduced.dk $(DIR)/$(PDIR)/%.ctx.dk fo.dko NJ.dko intuitionistic/zen.dko
. reduce.sh && check_nj "$(DIR)/$(PDIR)/$*"
#NAME NJ.
(; Loader ;)
Load : Type.
(; Intuitionistic Natural Deduction for Polymorphic Predicate Logic with equality ;)
true_intro : fo.proof fo.True.
def false_elim : p : fo.prop -> fo.proof fo.False -> fo.proof p.
and_intro : p : fo.prop ->
q : fo.prop ->
fo.proof p ->
fo.proof q ->
fo.proof (fo.and p q).
def and_elim1 : p : fo.prop ->
q : fo.prop ->
fo.proof (fo.and p q) ->
fo.proof p.