Commit 088da09b authored by Francois THIRE's avatar Francois THIRE

Merge branch 'master' of https://git.lsv.fr/genestier/PleinDeDk

parents 332a7d9b e7155360
......@@ -13,4 +13,5 @@ iProverModulo/*
dklib-master/*
TermChecker/*.txt
temp/*
*.tmp
\ No newline at end of file
*.tmp
*.tar*
\ No newline at end of file
......@@ -43,4 +43,7 @@ def andb : n : Nat -> Bool_ n.
[] e 0 (andb 0 ) --> True.
[x] e 0 (andb (S 0) x ) --> x.
[x,y,n] e n (andb _ x y) --> andb (S n) (and x y).
(; ;)
\ No newline at end of file
(; ;)
def g : n: Nat -> Bool_ n -> Bool.
[X] g (S (S (S 0))) X --> X True False True.
\ No newline at end of file
......@@ -13,8 +13,8 @@ Pos : Nat -> Int.
Neg : Nat -> Int.
def ifThenElse : Bool -> Int -> Int -> Int.
[x] ifThenElse T x _ --> x.
[y] ifThenElse F _ y --> y.
[x] ifThenElse Nat.T x _ --> x.
[y] ifThenElse Nat.F _ y --> y.
def plus : Int -> Int -> Int.
[x] plus x 0 --> x.
......
......@@ -18,30 +18,30 @@ 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.
[F] dx (x => y => F x) --> x:R => y:R => (d (x => F x)) x.
[F] dx (x => y => F y) --> x:R => y:R => 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.
[F] dy (x => y => F x) --> x:R => y:R => 0.
[F] dy (x => y => F y) --> x:R => y:R => (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).
[F] grad F --> x:R => y:R => 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] plus F G --> (x:R => y:R => 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).
x:R => y:R => p ((dx (x:R => y:R => F x y)) x y)
((dx (x:R => y:R => 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).
x:R => y:R => p ((dy (x:R => y:R => F x y)) x y)
((dy (x:R => y:R => G x y)) x y).
def trans : (R -> R -> R) -> (R -> R -> R).
[F] trans F --> x => y => F y x.
[F] trans F --> x:R => y:R => 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).
[F,G] flip (x => y => pair (F x y) (G x y)) --> x:R => y:R => 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).
......
#NAME NatInductor.
type: Type.
nat : type.
eps : type -> Type.
0 : eps nat.
s : eps nat -> eps nat.
def natind: P: (eps nat -> type) -> eps (P 0) -> (n: eps nat -> eps (P n) -> eps (P (s n))) -> m: (eps nat) -> eps (P m).
[P,h0,hs] natind P h0 hs 0 --> h0.
[P,h0,hs,m] natind P h0 hs (s m) --> hs m (natind P h0 hs m).
......@@ -19,3 +19,12 @@ def eps : eta prop -> Type.
[A, f] eps (forall A f) --> x:eta A -> eps (f x).
[l, r] eps (impl l r) --> eps l -> eps r.
(; Rien n'interdit d'ajouter un jour, ce qui justifie de refuser la règle eps (forall A f)
e : type.
def phi : eta e -> eta prop.
[x] phi x --> forall e phi.
(; Cette règle est terminante et ne fait aucun appel à eps, donc est entièrement disjointe de la règle eps (forall A f) dans le call graph ;)
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment