Permalink
Browse files

Add equiv test cases for cong.fsx, equal.fsx and order.fsx

146 tests passed
Time taken: 35.82 s
  • Loading branch information...
dungpa committed Oct 4, 2012
1 parent 0ddaa0f commit c526d0e226b09d4674d06dbb0b9b6cbc1b83e214
@@ -58,6 +58,9 @@
<Compile Include="resolution.fs" />
<Compile Include="prolog.fs" />
<Compile Include="meson.fs" />
+ <Compile Include="equal.fs" />
+ <Compile Include="cong.fs" />
+ <Compile Include="order.fs" />
</ItemGroup>
<ItemGroup>
<Reference Include="FSharpx.Compatibility.OCaml">
@@ -0,0 +1,38 @@
+// ========================================================================= //
+// Copyright (c) 2003-2007, John Harrison. //
+// Copyright (c) 2012 Eric Taucher, Jack Pappas, Anh-Dung Phan //
+// (See "LICENSE.txt" for details.) //
+// ========================================================================= //
+
+namespace Reasoning.Automated.Harrison.Handbook.Tests
+
+module cong =
+ open NUnit.Framework
+ open FsUnit
+
+ open Reasoning.Automated.Harrison.Handbook.lib
+ open Reasoning.Automated.Harrison.Handbook.formulas
+ open Reasoning.Automated.Harrison.Handbook.prop
+ open Reasoning.Automated.Harrison.Handbook.stal
+ open Reasoning.Automated.Harrison.Handbook.folMod
+ open Reasoning.Automated.Harrison.Handbook.skolem
+ open Reasoning.Automated.Harrison.Handbook.meson
+ open Reasoning.Automated.Harrison.Handbook.equal
+ open Reasoning.Automated.Harrison.Handbook.cong
+
+ // pg. 253
+ // ------------------------------------------------------------------------- //
+ // Example. //
+ // ------------------------------------------------------------------------- //
+
+ [<Test>]
+ let ``test ccvalid 1``() =
+ ccvalid (parse "f(f(f(f(f(c))))) = c /\ f(f(f(c))) = c
+ ==> f(c) = c \/ f(g(c)) = g(f(c))")
+ |> should be FsUnit.True
+
+ [<Test>]
+ let ``test ccvalid 2``() =
+ ccvalid (parse "f(f(f(f(c)))) = c /\ f(f(c)) = c ==> f(c) = c")
+ |> should be FsUnit.False
+
@@ -0,0 +1,58 @@
+// ========================================================================= //
+// Copyright (c) 2003-2007, John Harrison. //
+// Copyright (c) 2012 Eric Taucher, Jack Pappas, Anh-Dung Phan //
+// (See "LICENSE.txt" for details.) //
+// ========================================================================= //
+
+namespace Reasoning.Automated.Harrison.Handbook.Tests
+
+module equal =
+ open NUnit.Framework
+ open FsUnit
+
+ open Reasoning.Automated.Harrison.Handbook.lib
+ open Reasoning.Automated.Harrison.Handbook.formulas
+ open Reasoning.Automated.Harrison.Handbook.folMod
+ open Reasoning.Automated.Harrison.Handbook.skolem
+ open Reasoning.Automated.Harrison.Handbook.meson
+ open Reasoning.Automated.Harrison.Handbook.equal
+
+ // pg. 241
+ // ------------------------------------------------------------------------- //
+ // A simple example (see EWD1266a and the application to Morley's theorem). //
+ // ------------------------------------------------------------------------- //
+
+ [<Test>]
+ let ``test meson002 1``() =
+ equalitize (parse "
+ (forall x. f(x) ==> g(x)) /\
+ (exists x. f(x)) /\
+ (forall x y. g(x) /\ g(y) ==> x = y)
+ ==> forall y. g(y) ==> f(y)")
+ |> meson002
+ |> should FsUnit.equal [6]
+
+ [<Test>]
+ let ``test meson002 2``() =
+ equalitize (parse "forall c. f(f(f(f(f(c))))) = c /\ f(f(f(c))) = c ==> f(c) = c")
+ |> meson002
+ |> should FsUnit.equal [8]
+
+ [<Test>]
+ let ``test meson002 3``() =
+ (parse "
+ axiom(f(f(f(f(f(c))))),c) /\
+ axiom(c,f(f(f(f(f(c)))))) /\
+ axiom(f(f(f(c))),c) /\
+ axiom(c,f(f(f(c)))) /\
+ (forall s t. axiom(s,t) ==> achain(s,t)) /\
+ (forall s t. cong(s,t) ==> cchain(s,t)) /\
+ (forall s t u. axiom(s,t) /\ (t = u) ==> achain(s,u)) /\
+ (forall s t u. cong(s,t) /\ achain(t,u) ==> cchain(s,u)) /\
+ (forall s t. cchain(s,t) ==> s = t) /\
+ (forall s t. achain(s,t) ==> s = t) /\
+ (forall t. t = t) /\
+ (forall x y. x = y ==> cong(f(x),f(y)))
+ ==> f(c) = c")
+ |> meson002
+ |> should FsUnit.equal [17]
@@ -0,0 +1,36 @@
+// ========================================================================= //
+// Copyright (c) 2003-2007, John Harrison. //
+// Copyright (c) 2012 Eric Taucher, Jack Pappas, Anh-Dung Phan //
+// (See "LICENSE.txt" for details.) //
+// ========================================================================= //
+
+namespace Reasoning.Automated.Harrison.Handbook.Tests
+
+module order =
+ open NUnit.Framework
+ open FsUnit
+
+ open Reasoning.Automated.Harrison.Handbook.lib
+ open Reasoning.Automated.Harrison.Handbook.folMod
+ open Reasoning.Automated.Harrison.Handbook.order
+
+ let s = parset "f(x,x,x)"
+ let t = parset "g(x,y)"
+
+ [<Test>]
+ let ``test termsize 1``() =
+ termsize s > termsize t
+ |> should be FsUnit.True
+
+ // ------------------------------------------------------------------------- //
+ // This fails the rewrite properties. //
+ // ------------------------------------------------------------------------- //
+
+ let i = "y" |=> parset "f(x,x,x)"
+
+ [<Test>]
+ let ``test termsize 2``() =
+ termsize (tsubst i s) > termsize (tsubst i t)
+ |> should be FsUnit.False
+
+
@@ -7,7 +7,9 @@ Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Examples", "Examples", "{F3
ProjectSection(SolutionItems) = preProject
Examples\bdd.fsx = Examples\bdd.fsx
Examples\combining.fsx = Examples\combining.fsx
+ Examples\completion.fsx = Examples\completion.fsx
Examples\complex.fsx = Examples\complex.fsx
+ Examples\cong.fsx = Examples\cong.fsx
Examples\cooper.fsx = Examples\cooper.fsx
Examples\decidable.fsx = Examples\decidable.fsx
Examples\defcnf.fsx = Examples\defcnf.fsx

0 comments on commit c526d0e

Please sign in to comment.