From d31898173bbb70983a2277e63e924ac8c18fec2b Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 5 Feb 2020 12:32:13 -0600 Subject: [PATCH] remove coq tests besides Logic and nat_ind, add expeted output for those --- prover/t/And.v | 2 - prover/t/AndComm.v | 10 ----- prover/t/False_ind.v | 3 -- prover/t/Four.v | 7 ---- prover/t/Logic.v.expected | 84 +++++++++++++++++++++++++++++++++++++ prover/t/Or.v | 3 -- prover/t/nat_ind.v.expected | 30 +++++++++++++ 7 files changed, 114 insertions(+), 25 deletions(-) delete mode 100644 prover/t/And.v delete mode 100644 prover/t/AndComm.v delete mode 100644 prover/t/False_ind.v delete mode 100644 prover/t/Four.v create mode 100644 prover/t/Logic.v.expected delete mode 100644 prover/t/Or.v create mode 100644 prover/t/nat_ind.v.expected diff --git a/prover/t/And.v b/prover/t/And.v deleted file mode 100644 index 0922f5013..000000000 --- a/prover/t/And.v +++ /dev/null @@ -1,2 +0,0 @@ -Inductive and (A B : Prop) : Prop := - conj : forall (x : A), forall (y : B), and A B . diff --git a/prover/t/AndComm.v b/prover/t/AndComm.v deleted file mode 100644 index f2037a45b..000000000 --- a/prover/t/AndComm.v +++ /dev/null @@ -1,10 +0,0 @@ -Definition AndComm := - fun (A B : Prop) (H : and A B) => - match H with - conj H0 H1 => conj H1 H0 - end . - -// exists H0, H1. H = conj(H0, H1) /\ conj(H1, H0) - - -// desugarMatch(H, (conj(H0, H1), conj(H1, H0)), ... ) diff --git a/prover/t/False_ind.v b/prover/t/False_ind.v deleted file mode 100644 index e10e975d3..000000000 --- a/prover/t/False_ind.v +++ /dev/null @@ -1,3 +0,0 @@ -Definition False_ind := -fun (P : Prop) (f : False) => match f return P with - end . diff --git a/prover/t/Four.v b/prover/t/Four.v deleted file mode 100644 index 3dd65757b..000000000 --- a/prover/t/Four.v +++ /dev/null @@ -1,7 +0,0 @@ -Definition Four := 4 . - -// Definition AndComm := -// fun (A B : Prop) (H : A /\ B) => -// match H with -// | conj H0 H1 => conj H1 H0 -// end . diff --git a/prover/t/Logic.v.expected b/prover/t/Logic.v.expected new file mode 100644 index 000000000..e70bbc419 --- /dev/null +++ b/prover/t/Logic.v.expected @@ -0,0 +1,84 @@ + + + .CoqSentences + + + 1 + + + .GoalCellSet + + + + axiom \equals ( AndComm , \lambda { A { Term } , B { Term } , H { Term } , .Patterns } \or ( \exists { H0 , H1 , .Patterns } \and ( \equals ( H , conj ( H0 , H1 , .Patterns ) ) , conj ( H1 , H0 , .Patterns ) , .Patterns ) , .Patterns ) ) + + axiom \equals ( IF_then_else , or ( and , P , Q , .Patterns ) ( and , not , P , R , .Patterns ) ) + + axiom \equals ( iff , and ( \forall { x { Term } , .Patterns } B , .Patterns ) ( \forall { y { Term } , .Patterns } A , .Patterns ) ) + + axiom \equals ( not , \lambda { A { Term } , .Patterns } \forall { x { Term } , .Patterns } False ) + + axiom \type ( I ( .Patterns ) , True ) + + axiom \type ( S ( .Patterns ) , nat ( - , > , nat , .Patterns ) ) + + axiom \type ( Z ( .Patterns ) , nat ) + + axiom \type ( conj ( .Patterns ) , \forall { x { Term } , .Patterns } \forall { y { Term } , .Patterns } ( and ( A , B , .Patterns ) ) ) + + axiom \type ( ex_intro1 ( .Patterns ) , \forall { x { Term } , .Patterns } \forall { y { Term } , .Patterns } ( ex1 ( A , P , .Patterns ) ) ) + + axiom \type ( ex_intro2 ( .Patterns ) , \forall { x { Term } , .Patterns } \forall { y { Term } , .Patterns } ( ex2 ( P , .Patterns ) ) ) + + axiom \type ( ex_intro4 ( .Patterns ) , \forall { x { Term } , .Patterns } \forall { y { Term } , .Patterns } ( ex4 ( A , .Patterns ) ( P , .Patterns ) ) ) + + axiom \type ( or_introl ( .Patterns ) , \forall { x { Term } , .Patterns } ( or ( A , B , .Patterns ) ) ) + + axiom \type ( or_intror ( .Patterns ) , \forall { y { Term } , .Patterns } ( or ( A , B , .Patterns ) ) ) + + sort Term + + symbol AndComm ( .Sorts ) : Term + + symbol False ( .Sorts ) : Term + + symbol I ( .Sorts ) : Term + + symbol IF_then_else ( .Sorts ) : Term + + symbol S ( .Sorts ) : Term + + symbol True ( .Sorts ) : Term + + symbol Z ( .Sorts ) : Term + + symbol and ( .Sorts ) : Term + + symbol conj ( .Sorts ) : Term + + symbol ex1 ( .Sorts ) : Term + + symbol ex2 ( .Sorts ) : Term + + symbol ex4 ( .Sorts ) : Term + + symbol ex_intro1 ( .Sorts ) : Term + + symbol ex_intro2 ( .Sorts ) : Term + + symbol ex_intro4 ( .Sorts ) : Term + + symbol iff ( .Sorts ) : Term + + symbol nat ( .Sorts ) : Term + + symbol not ( .Sorts ) : Term + + symbol or ( .Sorts ) : Term + + symbol or_introl ( .Sorts ) : Term + + symbol or_intror ( .Sorts ) : Term + + + diff --git a/prover/t/Or.v b/prover/t/Or.v deleted file mode 100644 index 52ab7940a..000000000 --- a/prover/t/Or.v +++ /dev/null @@ -1,3 +0,0 @@ -Inductive or (A B : Prop) : Prop := - or_introl : forall (x : A), or A B - | or_intror : forall (y : A), or A B . diff --git a/prover/t/nat_ind.v.expected b/prover/t/nat_ind.v.expected new file mode 100644 index 000000000..d64c4c59b --- /dev/null +++ b/prover/t/nat_ind.v.expected @@ -0,0 +1,30 @@ + + + .CoqSentences + + + 1 + + + .GoalCellSet + + + + axiom \equals ( nat_ind , \lambda { P { Term } , f { Term } , f0 { Term } , .Patterns } \mu { F {{ Term }} , .Patterns } \lambda { n { Term } , .Patterns } \or ( \exists { .Patterns } \and ( \equals ( n , Z ) , f , .Patterns ) , \exists { n0 , .Patterns } \and ( \equals ( n , S ( n0 , .Patterns ) ) , f0 ( n0 , F , n0 , .Patterns ) , .Patterns ) , .Patterns ) ) + + axiom \type ( S ( .Patterns ) , \forall { x { Term } , .Patterns } nat ) + + axiom \type ( Z ( .Patterns ) , nat ) + + sort Term + + symbol S ( .Sorts ) : Term + + symbol Z ( .Sorts ) : Term + + symbol nat ( .Sorts ) : Term + + symbol nat_ind ( .Sorts ) : Term + + +