diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..ba0430d --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +__pycache__/ \ No newline at end of file diff --git a/checker/context.py b/checker/context.py index fd02dc9..7572afa 100644 --- a/checker/context.py +++ b/checker/context.py @@ -30,6 +30,12 @@ class Context: def empty(cls): return cls(props=set()) + def isempty(self) -> bool: + """ + Determine whether the context is empty. + """ + return len(self.props) == 0 + def issubseteq(self, other : Context) -> bool: """ Determine whether this context is a subset of another context. diff --git a/checker/lib/__init__.py b/checker/lib/__init__.py new file mode 100644 index 0000000..3a0415b --- /dev/null +++ b/checker/lib/__init__.py @@ -0,0 +1,10 @@ +""" + The library contains basic functions and proofs that you might want to + rely on. +""" + +from .basic import kernel_from_int + +__all__ = [ + "kernel_from_int", +] \ No newline at end of file diff --git a/checker/lib/basic.py b/checker/lib/basic.py new file mode 100644 index 0000000..a0561e2 --- /dev/null +++ b/checker/lib/basic.py @@ -0,0 +1,74 @@ +""" + Library containing all the basic functions +""" + +# from ..proof import Context, Proof +from ..props import Eq, Or, Prop +from ..terms import App, Const, EqT, Lambda, Term, Var, register_known_const + +# ----------------------------------------------------------------------------- +# Identity function +# ----------------------------------------------------------------------------- +# Always returns its input. +register_known_const("identity", Lambda(Var(0))) + +# ----------------------------------------------------------------------------- +# Equality +# ----------------------------------------------------------------------------- +equality = Lambda(Lambda(EqT(lhs=Var(1), rhs=Var(0)))) + +register_known_const("eq", equality) +register_known_const("==", equality) + +# ----------------------------------------------------------------------------- +# Bool +# ----------------------------------------------------------------------------- + +bool_t = Lambda(Lambda(Var(1))) +bool_f = Lambda(Lambda(Var(0))) +if_statement = Lambda(Var(0)) +not_statement = Lambda(App(f=App(f=Var(0), x=bool_f), x=bool_t)) + +register_known_const("Bool.False", bool_f) +register_known_const("Bool.True", bool_t) +register_known_const("Bool.elim", if_statement) +register_known_const("Bool.if", if_statement) +register_known_const("Bool.not", not_statement) + +def is_bool(x : Term) -> Prop: + return Or(Eq(x=x, y=bool_f), Eq(x=x, y=bool_t)) + +# ----------------------------------------------------------------------------- +# Nat +# ----------------------------------------------------------------------------- + +zero = Const("Nat.Zero") +succ = Const("Nat.Succ") + +def kernel_from_int(n : int) -> Term: + if n < 0: + raise ValueError( + "Int is not Nat" + ) + elif n == 0: + return zero + else: + return App(f=succ, x=kernel_from_int(n-1)) + +def is_nat(x : Term) -> Prop: + return Or( + Eq(x=x, y=zero), + Eq(bool_f, bool_t) # TODO: Construct x = Succ n where isNat(n), + ) + +register_known_const("Nat.add", Lambda(Lambda( + App(f=App( # If-statement: is the first argument zero? + f=EqT(lhs=Var(1), rhs=zero), + # If so, return the second argument + x=Var(0), + ), + # If not, return a recursive solution of the add function + # TODO: Not correct yet + x=App(f=succ, x=App(f=App(f=Const("Nat.add"), x=Var(1)), x=Var(0))) + ) +))) diff --git a/checker/proof.py b/checker/proof.py index 2a083db..d218981 100644 --- a/checker/proof.py +++ b/checker/proof.py @@ -20,6 +20,19 @@ class Proof: context : Context statement : Prop + def check(self) -> None: + """ + Check whether the proof is self-sufficient. That is, the proof + relies on zero context in order to be considered true. + """ + if self.context.isempty(): + return + + else: + raise ProofCheckerFailedException( + f"Proof still relies on {len(self.context.props)} assumptions." + ) + def and_l(proof : Proof, a : Prop, b : Prop) -> Proof: """ Create a proof that collects two hypotheses and collects them in a @@ -117,6 +130,54 @@ def from_assumption(ctx : Context, statement : Prop) -> Proof: return Proof(context=ctx, statement=statement) +def or_l(proof_a : Proof, proof_b : Proof, a : Prop, b : Prop) -> Proof: + """ + Create a proof that builds a generalized OR-statement in the context. + + $$ + Γ, A ⊢ C Γ, B ⊢ C + ---------------------- + Γ, A ∨ B ⊢ C + $$ + + :param proof_a: The first proof. + :type proof_a: Proof + :param proof_b: The second proof. + :type proof_b: Proof + :param a: The proposition from the first proof. + :type a: Prop + :param b: The proposition from the second proof. + :type b: Prop + :return: A proof demonstrating a statement given that either proposition + a or b is true. + :rtype: Proof + """ + statement = proof_a.statement + + if statement != proof_b.statement: + raise ProofCheckerFailedException( + "For proof constructor `or_l`, the statements of the two proofs " + "must match: {proof_a.statement} and {proof_b.statement} do not " + "match." + ) + if not proof_a.context.contains(a): + raise ProofCheckerFailedException( + f"Proposition {a} not found in context of the first proof." + ) + if not proof_b.context.contains(b): + raise ProofCheckerFailedException( + f"Proposition {b} not found in context of the second proof." + ) + + return Proof( + context=( + proof_a.context.union(proof_b.context) + .without_prop(a).without_prop(b).with_prop(Or(a, b)) + ), + statement=proof_a.statement, + ) + + def or_r(proof : Proof, a : Prop, b : Prop) -> Proof: """ Create a proof that demonstrates that a generalization is true. diff --git a/checker/props.py b/checker/props.py index 2fd8cfe..6e13958 100644 --- a/checker/props.py +++ b/checker/props.py @@ -50,6 +50,7 @@ class And(Prop): P : Prop Q : Prop +@dataclass(frozen=True) class Eq(Prop): """ Compare whether two terms are equal. diff --git a/checker/terms.py b/checker/terms.py index 482ce45..3890b3d 100644 --- a/checker/terms.py +++ b/checker/terms.py @@ -9,11 +9,10 @@ import copy from dataclasses import dataclass -__known_consts : dict[str, Term] = { -} +_known_consts : dict[str, Term] = {} def register_known_const(name : str, value : Term) -> None: - __known_consts[name] = value + _known_consts[name] = value class Term: """ @@ -119,11 +118,30 @@ class Const(Term): name : str def normalize(self) -> Term: - if self.name in __known_consts: - return copy.deepcopy(__known_consts.get(self.name, self)) + if self.name in _known_consts: + return copy.deepcopy(_known_consts.get(self.name, self)) else: return self +@dataclass(frozen=True) +class EqT(Term): + """ + Equality operator. Possibly the only function that is implemented into + the core of the term definitions. + """ + + lhs : Term + rhs : Term + + def normalize(self) -> Term: + l = self.lhs.normalize() + r = self.rhs.normalize() + + if l == r: + return Const("Bool.True") + else: + return Const("Bool.False") + @dataclass(frozen=True) class Lambda(Term): """ diff --git a/low.c b/low.c deleted file mode 100644 index 6328778..0000000 --- a/low.c +++ /dev/null @@ -1,529 +0,0 @@ -#include -#include -#include -#include - -// Structures defined in this file -typedef struct BlockHeader BlockHeader; -typedef struct Closure Closure; -typedef struct Frame Frame; -typedef struct Text Text; -typedef struct UnionType UnionType; -typedef struct Var Var; - -// You can change this number to decide how much memory the program is allowed -// 0 - 193 bytes -> The program refuses to start -// 194 - 217 bytes -> The program starts but doesn't do anything -// 218 + bytes -> The program runs successfully -#define MEM_SIZE 193 //1024 * 1024 // 1 MB - -#define EXIT_GRACEFULLY 0 -#define EXIT_MEMORY_LIMIT_TOO_LOW 11 -#define EXIT_COULD_NOT_INIT_MEMORY 12 -#define EXIT_OUT_OF_MEMORY_DURING_INITIALIZATION 13 - -#define EXIT_IMPOSSIBLE_FUNCTION_PHASE 77 -#define EXIT_IMPOSSIBLE_FUNCTION_ID 78 -#define EXIT_IMPOSSIBLE_FUNCTION_NO_CONTINUATION 79 - -#define EXIT_IF_NULL(ptr) ({ \ - if (!ptr) { \ - free(memory); \ - printf("Failed to initialize program: out of memory\n"); \ - exit(EXIT_OUT_OF_MEMORY_DURING_INITIALIZATION); \ - } \ -}) - -/* ============================================================================ - * MEMORY - * ============================================================================ - */ - -// Memory block structure -// This block functions as a header for memory allocations on the heap -typedef struct BlockHeader { - int free; - struct BlockHeader *next; -} BlockHeader; - -#define BLOCK_SIZE(header) ({ \ - size_t s; \ - if (header->next) { \ - s = (uint8_t *)(header->next) - (uint8_t *)header; \ - } else { \ - s = (uint8_t *)(stack_top) - (uint8_t *)header; \ - } \ - s - sizeof(BlockHeader); \ -}) - -// Global memory pool -static uint8_t *memory = NULL; -static uintptr_t heap_base; -static uintptr_t heap_top; -static uintptr_t stack_base; -static uintptr_t stack_top; - -// Initialize the custom memory manager -void init_memory() { - if (MEM_SIZE < sizeof(BlockHeader) + 1) { - printf("Memory limit is too low!\n"); - exit(EXIT_MEMORY_LIMIT_TOO_LOW); - } - - memory = (uint8_t *)malloc(MEM_SIZE); - if (!memory) { - printf("Memory allocation failed!\n"); - exit(EXIT_COULD_NOT_INIT_MEMORY); - } - heap_base = (uintptr_t)memory; - heap_top = heap_base; - stack_base = (uintptr_t)(memory + MEM_SIZE); - stack_top = stack_base; - - BlockHeader *curr = (BlockHeader *)heap_base; - curr->free = 1; - curr->next = NULL; -} - -// Macro for allocating a number of bytes on the heap -#define HEAP_ALLOC(nbytes) ({ \ - void *ptr = NULL; \ - BlockHeader *curr = (BlockHeader *)heap_base; \ - while(curr) { \ - size_t size = (BLOCK_SIZE(curr)); \ - if (curr->free && size >= (nbytes)) { \ - /* If there's enough memory left over, split off into two */ \ - if (size >= (nbytes) + sizeof(BlockHeader) + 1) { \ - BlockHeader *new_block = (BlockHeader *)( \ - (uint8_t *)curr + sizeof(BlockHeader) + (nbytes) \ - ); \ - new_block->free = 1; \ - new_block->next = curr->next; \ - curr->next = new_block; \ - if ((uint8_t *)heap_top < (uint8_t *)new_block) { \ - heap_top = (uintptr_t)new_block + sizeof(BlockHeader); \ - } \ - } \ - /* Assign block to new memory */ \ - curr->free = 0; \ - ptr = (uint8_t *)curr + sizeof(BlockHeader); \ - break; \ - } \ - /* Otherwise, go to the next block */ \ - curr = curr->next; \ - } \ - ptr; \ -}) - -// Macro for freeing bytes at a given address on the heap -#define HEAP_FREE(ptr) ({ \ - if (ptr) { \ - BlockHeader *block = (BlockHeader *)( \ - (uint8_t *)(ptr) - sizeof(BlockHeader) \ - ); \ - block->free = 1; \ - /* Merge adjacent free blocks */ \ - BlockHeader *curr = (BlockHeader *)heap_base; \ - while (curr) { \ - if (curr->free && curr->next && curr->next->free) { \ - curr->size += sizeof(BlockHeader) + curr->next->size; \ - curr->next = curr->next->next; \ - } else { \ - curr = curr->next; \ - } \ - } \ - } \ -}) - -// Pointer for debugging: print the heap to stdout -#define HEAP_PRINT_WIDTH 60 -#define HEAP_PRINT() ({ \ - BlockHeader *curr = (BlockHeader *)heap_base; \ - while (curr) { \ - size_t size = BLOCK_SIZE(curr); \ - printf("BlockHeader at address %ld (physical %p): %lu byte", \ - (uint8_t *)curr - memory, curr, size \ - ); \ - if (size == 1) { printf(" of "); } else { printf("s of "); } \ - if (curr->free) { \ - printf("free memory\n "); \ - } else { \ - printf("reserved memory\n "); \ - } \ - unsigned char *content = (uint8_t *)curr; \ - for (int i = 0; i < size + sizeof(BlockHeader); i++) { \ - if (i == sizeof(BlockHeader)) { printf("| "); } \ - printf("%02X ", content[i]); \ - if (i > HEAP_PRINT_WIDTH) { printf("..."); break; } \ - } \ - printf("\n "); \ - for (int i = 0; i < size + sizeof(BlockHeader); i++) { \ - if (i == sizeof(BlockHeader)) { printf("| "); } \ - if (content[i] == 0) { printf(" "); \ - } else if (content[i] >= 32 && content[i] < 127) { \ - printf("%c ", content[i]); \ - } else { printf("__ "); } \ - if (i > HEAP_PRINT_WIDTH) { printf("..."); break; } \ - } \ - printf("\n"); \ - curr = curr->next; \ - } \ -}) - -#define SPACE_FILL(n) for (int i=0; i= heap_top + (nbytes)) { \ - stack_top -= (nbytes); \ - ptr = (void *)stack_top; \ - } \ - ptr; \ -}) - -#define STACK_PRINT_VARIABLE_MAX 5 -#define STACK_PRINT(topPtr) ({ \ - Frame *cursor = topPtr; \ - while (cursor) { \ - Frame *next = cursor->cont; \ - size_t size; \ - if (next) { \ - size = (uint8_t *)(next) - (uint8_t *)(cursor); \ - } else { \ - size = (uint8_t *)(stack_base) - (uint8_t *)(cursor); \ - } \ - printf("Stack layer at offset -%ld (phsyical %p): %ld byte", \ - (uint8_t *)(stack_base) - (uint8_t *)(cursor), cursor, size \ - ); \ - if (size == 1) { printf("\n "); } else { printf("s\n "); } \ - unsigned char *content = (uint8_t *)cursor; \ - printf("| Code ID"); SPACE_FILL(sizeof(CodeID)*3 - 7 - 1); \ - printf("| Phase"); SPACE_FILL(sizeof(int)*3 - 5 - 2); \ - printf("| Prev out"); SPACE_FILL(sizeof(Var *)*3-8 - 2); \ - printf("| Continuation"); SPACE_FILL(sizeof(Frame *)*3-12 - 1); \ - for (int i = 0; i < size - sizeof(Frame); i++) { \ - printf("| Variable %d", i + 2); SPACE_FILL(2); \ - if (i + 2 == STACK_PRINT_VARIABLE_MAX) { break; } \ - } \ - printf("|\n | "); \ - for (int i = 0; i < sizeof(Frame); i++) { \ - printf("%02X ", content[i]); \ - } \ - for (int i = sizeof(Frame); i < size; i++) { \ - if ((i - sizeof(Frame)) % sizeof(Var) == 0) { printf("|"); } \ - printf("%02X ", content[i]); \ - if (i - sizeof(Frame) == STACK_PRINT_VARIABLE_MAX * sizeof(Var)) { \ - break; \ - } \ - } \ - printf("|\n"); \ - cursor = cursor->cont; \ - } \ -}) -// #define STACK_PRINT ({ \ -// printf("Stack from base %p to top %p:\n", (void *)stack_base, (void *)stack_top); \ -// uint8_t *curr = (uint8_t *)stack_top; \ -// while ((uintptr_t)curr < stack_base) { \ -// printf("Address %ld (physical %p): \n ", curr - memory, curr); \ -// for (int i = 0; i < STACK_PRINT_WIDTH && (uintptr_t)(curr + i) < stack_base; i++) { \ -// printf("%02X ", curr[i]); \ -// } \ -// printf("\n "); \ -// for (int i = 0; i < STACK_PRINT_WIDTH && (uintptr_t)(curr + i) < stack_base; i++) { \ -// if (curr[i] == 0) { \ -// printf(" "); \ -// } else if (curr[i] >= 32 && curr[i] < 127) { \ -// printf("%c ", curr[i]); \ -// } else { \ -// printf("__ "); \ -// } \ -// } \ -// printf("\n"); \ -// curr += STACK_PRINT_WIDTH; \ -// } \ -// }) - - -// Macro for freeing a number of bytes on the stack -#define STACK_FREE(nbytes) ({ \ - stack_top += (nbytes); \ -}) - -#define MEM_DIAGNOSTICS(curr) ({ \ - printf("----------------------------\n"); \ - printf("Heap base at address %ld (physical %p)\n", \ - (uint8_t *)heap_base - (uint8_t *)memory, (uint8_t *)heap_base \ - ); \ - printf("Heap top at address %ld (physical %p)\n", \ - (uint8_t *)heap_top - (uint8_t *)memory, (uint8_t *)heap_top \ - ); \ - HEAP_PRINT(); \ - printf("----------------------------\n"); \ - printf("Heap base at address %ld (physical %p)\n", \ - (uint8_t *)heap_base - (uint8_t *)memory, (uint8_t *)heap_base \ - ); \ - printf("Heap top at address %ld (physical %p)\n", \ - (uint8_t *)heap_top - (uint8_t *)memory, (uint8_t *)heap_top \ - ); \ - printf("Stack top at address %ld (physical %p)\n", \ - (uint8_t *)stack_top - (uint8_t *)memory, (uint8_t *)stack_top \ - ); \ - printf("Stack base at address %ld (physical %p)\n", \ - (uint8_t *)stack_base - (uint8_t *)memory, (uint8_t *)stack_base \ - ); \ - printf("----------------------------\n"); \ - if (curr) { \ - STACK_PRINT(curr); \ - } else { \ - printf("Stack is NULL!\n"); \ - } \ - printf("Stack top at address %ld (physical %p)\n", \ - (uint8_t *)stack_top - (uint8_t *)memory, (uint8_t *)stack_top \ - ); \ - printf("Stack base at address %ld (physical %p)\n", \ - (uint8_t *)stack_base - (uint8_t *)memory, (uint8_t *)stack_base \ - ); \ - printf("----------------------------\n"); \ -}) - - -/* ============================================================================ - * VARIABLES & VALUES - * ============================================================================ - */ - -// Types of values that can be stored in the heap -typedef union { - int i; - char c; - Closure *f; - Text *t; - UnionType *u; -} Value; - -#define HEAP_ALLOC_VALUE() HEAP_ALLOC(sizeof(Value)) - -// Types of variables stored in a frame -typedef enum { - ORIGINAL_VARIABLE, - MUTABLE_REFERENCE, - IMMUTABLE_REFERENCE -} VarType; - -// Variable -typedef struct Var { - VarType var_type; - Value *value; -} Var; - -#define HEAP_ALLOC_VARIABLE() HEAP_ALLOC(sizeof(Var)) - -// Names of functions -typedef enum { - CODE_F, - CODE_G, - CODE_H, - CODE_EXIT // Indicates termination -} CodeID; - -// A closure can represent a function that has yet to gather all inputs -typedef struct Closure { - CodeID code_id; - Var variables[]; -} Closure; - -// A Text struct represents a string -typedef struct Text { - size_t len; - char s[]; -} Text; - -// A Union type represents a type that can be one of several values. -// For example: -// type Maybe a = Just a | Nothing -typedef struct UnionType { - int name; - Value values[]; -} UnionType; - -#define HEAP_ALLOC_CLOSURE(code_id, arity) ({ \ - Closure *c = HEAP_ALLOC(sizeof(Closure) + arity * sizeof(Var)); \ - if (c) { \ - c->code_id = code_id; \ - } \ - c; \ -}) - -#define HEAP_ALLOC_TEXT(length) ({ \ - Text *t = HEAP_ALLOC(sizeof(Text) + length * sizeof(char)); \ - if (t) { \ - t->len = length; \ - for (int i = 0; i < length; i++) { \ - t->s[i] = '\0'; \ - } \ - } \ - t; \ -}) - -#define HEAP_ALLOC_UNION_TYPE(name, arity) ({ \ - UnionType *u = HEAP_ALLOC(sizeof(UnionType) + arity * sizeof(Value)); \ - if (u) { \ - u->name = name; \ - } \ - u; \ -}) - -// Function arity -#define ARITY_F 1 -#define ARITY_G 1 -#define ARITY_H 1 -#define ARITY_EXIT 1 - -typedef struct Frame { - // Function to execute - CodeID code_id; - - // Phase of the function - int phase; - - // Return variable from previous frame - Var *prevOut; - - // CPS-style next frame to execute - struct Frame *cont; - - // Previously captured variables - Var variables[]; -} Frame; - -#define FRAME_SIZE(arity) sizeof(Frame) + (arity - 1) * sizeof(Var) - -#define STACK_ALLOC_FRAME(code_name, arity) ({ \ - Frame *f = STACK_ALLOC(FRAME_SIZE(arity)); \ - if(f) { \ - f->code_id = code_name; \ - f->phase = 0; \ - f->prevOut = NULL; \ - f->cont = NULL; \ - } \ - f; \ -}) - -#define STACK_FREE_FRAME(arity) STACK_FREE(FRAME_SIZE(arity)) - -int main(void) { - init_memory(); - - Text *t = HEAP_ALLOC_TEXT(50); EXIT_IF_NULL(t); - Value *v = HEAP_ALLOC_VALUE(); EXIT_IF_NULL(v); - Var *var = HEAP_ALLOC_VARIABLE(); EXIT_IF_NULL(var); - Frame *fnsh = STACK_ALLOC_FRAME(CODE_EXIT, ARITY_EXIT); EXIT_IF_NULL(fnsh); - Frame *curr = STACK_ALLOC_FRAME(CODE_H, ARITY_H); EXIT_IF_NULL(curr); - - sprintf(t->s, "Kaokkokos shall prevail by the hands of Alkbaard!"); - - v->t = t; - var->var_type = ORIGINAL_VARIABLE; - var->value = v; - curr->prevOut = var; - curr->cont = fnsh; - - // STACK_PRINT(curr); - - while (curr) { - // MEM_DIAGNOSTICS(curr); - switch (curr->code_id) { - case CODE_F: { - // f(x) = print(x) and return x - Var *x = curr->prevOut; - Frame *next = curr->cont; - STACK_FREE_FRAME(ARITY_F); - - if (x) { - printf("%s\n", x->value->t->s); - } else { - printf("NULL: Out of memory!\n"); - } - - curr = next; - break; - } - case CODE_G: { - // g(x) = String.upper(x) - Var *x = curr->prevOut; - Frame *next = curr->cont; - STACK_FREE_FRAME(ARITY_G); - - if (x) { - for (int i = 0; i < x->value->t->len; i++) { - char c = x->value->t->s[i]; - if (c >= 'a' && c <= 'z') { - x->value->t->s[i] = c - ('a' - 'A'); - } - } - - next->prevOut = x; - } - - curr = next; - break; - } - case CODE_H : { - // h(x) = f(g(x)) - Var *x = curr->prevOut; - Frame *next = curr->cont; - STACK_FREE_FRAME(ARITY_H); - - if (x) { - Frame *f = STACK_ALLOC_FRAME(CODE_F, ARITY_F); - - if (f) { - Frame *g = STACK_ALLOC_FRAME(CODE_G, ARITY_G); - - if (g) { - f->cont = next; - - g->prevOut = x; - g->cont = f; - curr = g; - } else { - // No memory available! Free f & exit this function - STACK_FREE_FRAME(ARITY_F); - next->prevOut = NULL; - curr = next; - } - } else { - // No memory available! Exit this function - next->prevOut = NULL; - curr = next; - } - } else { - // prevOut is NULL - we were out of memory! - curr = next; - } - - break; - } - case CODE_EXIT: { - // HEAP_PRINT(); - free(memory); - exit(EXIT_GRACEFULLY); - break; - } - default: { - free(memory); - printf("ERROR: Reached impossible function id!\n"); - exit(EXIT_IMPOSSIBLE_FUNCTION_ID); - break; - } - } - } - - free(memory); - - printf("ERROR: Reached function with no continuation!\n"); - - return EXIT_IMPOSSIBLE_FUNCTION_NO_CONTINUATION; -} - diff --git a/proof.py b/proof.py deleted file mode 100644 index 0ad1db9..0000000 --- a/proof.py +++ /dev/null @@ -1,427 +0,0 @@ -from __future__ import annotations -from typing import Any, Callable, Union - -from dataclasses import dataclass - -# ----------------------------------------------------------------------------- -# Terms -# ----------------------------------------------------------------------------- - -class Term: - pass - -@dataclass(frozen=True) -class App(Term): - f : Term - x : Term - - def __repr__(self): - match self.f: - case App(f=Const("Nat.add"), x=a): - return f"{a} + {self.x}" - case App(f=Const("List.cons"), x=a): - return f"{a} :: {self.x}" - case Const("Nat.Succ"): - cursor, i = self, 0 - - while True: - match cursor: - case App(f=Const("Nat.Succ")): - cursor = cursor.x - i += 1 - case Const("Nat.Zero"): - return str(i) - case _: - xs = str(cursor) - if " " in xs: - xs = "(" + xs + ")" - return "{xs} + {i}" - case _: - fs = str(self.f) - xs = str(self.x) - - if " " in fs: - fs = "(" + fs + ")" - if " " in xs: - xs = "(" + xs + ")" - - return f"{fs} xs" - -A0 = lambda fn : Const(fn) -A1 = lambda fn, a : App(f=A0(fn), x=a) -A2 = lambda fn, a, b : App(f=A1(fn, a), x=b) -A3 = lambda fn, a, b, c : App(f=A2(fn, a, b), x=c) -A4 = lambda fn, a, b, c, d : App(f=A3(fn, a, b, c), x=d) -A5 = lambda fn, a, b, c, d, e : App(f=A4(fn, a, b, c, d), x=e) -A6 = lambda fn, a, b, c, d, e, f : App(f=A5(fn, a, b, c, d, e), x=f) -A7 = lambda fn, a, b, c, d, e, f, g : App(f=A6(fn, a, b, c, d, e, f), x=g) -A8 = lambda fn, a, b, c, d, e, f, g, h : App(f=A7(fn, a, b, c, d, e, f, g), x=h) - -@dataclass(frozen=True) -class Const(Term): - name : str - - def __repr__(self) -> str: - match self.name: - case "List.Nil": - return "[]" - case "Nat.Zero": - return "0" - case _: - return self.name - -# --- Bool constructors --- - -def Truth() -> Term: - return A0("Bool.Truth") - -def Contradiction() -> Term: - return A0("Bool.Contradiction") - -# --- List constructors --- - -def Nil() -> Term: - return A0("List.Nil") - -def Cons(head : Term, tail : Term) -> Term: - return A2("List.Cons", head, tail) - -# --- Nat constructors --- - -def Zero() -> Term: - return A0("Nat.Zero") - -def Succ(n : Term) -> Term: - return A1("Nat.Succ", n) - -def kernel_from_int(n : int) -> Term: - if n == 0: - return Zero() - elif n < 0: - raise ValueError("Int is not Nat") - else: - return Succ(kernel_from_int(n-1)) - -# ----------------------------------------------------------------------------- -# Propositions -# ----------------------------------------------------------------------------- - -class Prop: - pass - -@dataclass(frozen=True) -class Contradict(Prop): - s : str - -@dataclass(frozen=True) -class Eq(Prop): - lhs : Term - rhs : Term - -@dataclass(frozen=True) -class Trivial(Prop): - pass - # def __repr__(self) -> str: - # return "" - -# ----------------------------------------------------------------------------- -# Proofs -# ----------------------------------------------------------------------------- - -class Proof: - def apply(self, goal : Prop, ctx : Context) -> Prop: - return ( - Contradict("Cannot prove using the base class") - ) - -@dataclass(frozen=True) -class Assumption(Proof): - def apply(self, goal : Prop, ctx : Context) -> Prop: - return ( - Trivial() if goal in ctx.props else - Contradict(f"Couldn't find proposition `{goal}` in assumptions") - ) - - -@dataclass(frozen=True) -class Refl(Proof): - def apply(self, goal : Prop, ctx : Context) -> Prop: - match goal: - case Contradict(): - return goal - - case Eq(): - l = normalize(goal.lhs) - r = normalize(goal.rhs) - - if l == r: - return Trivial() - else: - # Reduce to differing parts - while True: - match ( l, r ): - case ( App(), App() ): - if l.x == r.x: - l, r = l.f, r.f - elif l.f == r.f: - l, r = l.x, r.x - else: - break - case _: - break - - return Contradict( - f"Couldn't normalize {goal.lhs} = {goal.rhs} any further than to {l} = {r}" - ) - - case Trivial(): - return goal - - case Prop(): - return goal - -@dataclass(frozen=True) -class Rewrite(Proof): - m : Term - s : Term - - def apply(self, goal : Prop, ctx : Context) -> Prop: - if Eq(lhs=self.m, rhs=self.s) not in ctx.props: - if Eq(lhs=self.s, rhs=self.m) not in ctx.props: - return Contradict( - f"Could not find justification why you would be able to substitute {self.m} with {self.s}" - ) - - match goal: - case Contradict(): - return goal - - case Eq(lhs=lhs, rhs=rhs): - return Eq( - lhs=self.find_and_replace(lhs), - rhs=self.find_and_replace(rhs), - ) - - case Prop(): - return goal - - case Trivial(): - return goal - - def find_and_replace(self, term : Term) -> Term: - if term == self.m or term == self.s: - return self.s - - match term: - case App(f=f, x=x): - return App( - f=self.find_and_replace(f), - x=self.find_and_replace(x), - ) - - case Const(): - return term - - case Term(): - return term - -@dataclass(frozen=True) -class Script(Proof): - steps : list[Proof] - - def apply(self, goal: Prop, ctx: Context) -> Prop: - state = goal - - for step in self.steps: - state = step.apply(state, ctx) - - return state - -# ----------------------------------------------------------------------------- -# Context -# ----------------------------------------------------------------------------- -# The context is a set of information you already know. - -@dataclass(frozen=True) -class Context: - props : list[Prop] - - def with_prop(self, prop : Prop): - return Context([ p for p in self.props ] + [ prop ]) - -# ----------------------------------------------------------------------------- -# Normalization function -# ----------------------------------------------------------------------------- - -@dataclass(frozen=True) -class F: - arity : int - func : Callable[..., Term | None] - -F_ = lambda a : lambda f : F(arity=a, func=f) -F0, F1, F2, F3 = F_(0), F_(1), F_(2), F_(3) -F4, F5, F6, F7 = F_(4), F_(5), F_(6), F_(7) - -def apply_rules() -> dict[str, F]: - def __bool_not(x : Term) -> Term | None: - match x: - case Const("Bool.Truth"): - return Contradiction() - - case Const("Bool.Contradiction"): - return Truth() - - def __list_isempty(x : Term) -> Term | None: - match x: - case Const("List.Nil"): - return Truth() - - case App(f=App(f=Const("List.Cons"))): - return Contradiction() - - def __list_length(x : Term) -> Term | None: - match x: - case Const("List.Nil"): - return Zero() - - case App(f=App(f=Const("List.Cons"), x=head), x=tail): - return Succ(A1("List.length", tail)) - - def __nat_add(x : Term, y : Term) -> Term | None: - match x: - case Const("Nat.Zero"): - return y - - case App(f=Const("Nat.Succ"), x=x_): - return Succ(A2("Nat.add", x_, y)) - - def __nat_iszero(x : Term) -> Term | None: - match x: - case Const("Nat.Zero"): - return Truth() - - case App(f=Const("Nat.Succ")): - return Contradiction() - - return { - "Bool.not": F1(__bool_not), - "List.isEmpty": F1(__list_isempty), - "List.length": F1(__list_length), - "Nat.add" : F2(__nat_add), - "Nat.isZero" : F1(__nat_iszero), - } - -def normalize(term : Term) -> Term: - match term: - case App(): - f = normalize(term.f) - x = normalize(term.x) - - cursor = term - items = [ term ] - - while True: - match cursor.f: - case App(): - cursor = cursor.f - items.append(cursor) - - case Const(): - name = cursor.f.name - rule = apply_rules().get(name, None) - - if rule is None: - return App(f, x) # Unknown function - if len(items) != rule.arity: - # If len(items) is too small, we don't have - # enough inputs yet to evaluate the function - # If len(items) is too large, we already evaluated - # the function before and couldn't optimize. - return App(f, x) - - out = rule.func(*reversed([i.x for i in items])) - - return normalize(out) if out is not None else App(f, x) - - case Const(): - return term - - case Term(): - return term - -# ----------------------------------------------------------------------------- -# Proof checker -# ----------------------------------------------------------------------------- - -ProofCheck = Union["Proven", "ProveFailure"] - -@dataclass(frozen=True) -class Proven: - pass - -@dataclass(frozen=True) -class ProveFailure: - s : str - -def check(goal: Prop, proof : Proof, ctx : Context) -> Prop: - return proof.apply(goal, ctx) - -# ----------------------------------------------------------------------------- -# ----------------------------------------------------------------------------- -# ----------------------------------------------------------------------------- - -if __name__ == "__main__": - # 2 + 3 == 5 - print(check( - Eq( - lhs=A2("Nat.add", kernel_from_int(2), kernel_from_int(3)), - rhs=kernel_from_int(5), - ), - Refl(), - Context(props=[]), - )) - - # 2 + 3 == 7 - print(check( - Eq( - lhs=A2("Nat.add", kernel_from_int(2), kernel_from_int(3)), - rhs=kernel_from_int(7), - ), - Refl(), - Context(props=[]), - )) - - # 0 + x == x - print(check( - Eq( - lhs=A2("Nat.add", Zero(), Const("x")), - rhs=Const("x") - ), - Refl(), - Context(props=[]), - )) - - # x + 0 == x - print(check( - Eq( - lhs=A2("Nat.add", Const("x"), Zero()), - rhs=Const("x") - ), - Refl(), - Context(props=[]), - )) - - # x + 4 = 6 when x = 2 - print(check( - goal=Eq( - lhs=A2("Nat.add", Const("x"), kernel_from_int(4)), - rhs=kernel_from_int(6), - ), - proof=Script([ - Rewrite(m=Const("x"), s=kernel_from_int(2)), - Refl() - ]), - ctx=Context([ - Eq(Const("x"), kernel_from_int(2)), - ]), - )) diff --git a/proof_checker.py b/proof_checker.py new file mode 100644 index 0000000..99d6c5d --- /dev/null +++ b/proof_checker.py @@ -0,0 +1,20 @@ +from checker import lib, proof, props +from checker.terms import App, Const + +# Prove : true == not false +p = proof.reflexivity( + props.Eq( + x=Const("Bool.True"), + y=App(f=Const("Bool.not"), x=Const("Bool.False")) + ) +) +p.check() + +# Prove : false == not true +p = proof.reflexivity( + props.Eq( + x=Const("Bool.False"), + y=App(f=Const("Bool.not"), x=Const("Bool.True")) + ) +) +p.check()