### A Pluto.jl notebook ###
# v0.14.5

using Markdown
using InteractiveUtils

# â•”â•�â•¡ 40dd03fa-bb9a-11eb-3a08-a30e7215415b
abstract type Prop end

# â•”â•�â•¡ 814f0f17-d918-4a5b-8504-4ad0f9ea25b1
begin
	abstract type âŠ¤ <: Prop end
	abstract type âŠ¥ <: Prop end
end

# â•”â•�â•¡ 90cecfc3-753b-4a4e-85aa-6bf8b6face58
begin
	abstract type â†’{Ï•, Ïˆ} <: Prop where {Ï• <: Prop, Ïˆ <: Prop} end
	â†’(::Type{Ï•}, ::Type{Ïˆ}) where {Ï• <: Prop, Ïˆ <: Prop} = â†’{Ï•, Ïˆ}
end

# â•”â•�â•¡ 035c180e-631f-4dc3-9c5e-d5fe4f0d865c
begin
	abstract type Â¬{Ï•} <: Prop where {Ï• <: Prop} end
	Â¬(::Type{Ï•}) where {Ï• <: Prop} = Â¬{Ï•} #Ï• â†’ âŠ¥
end

# â•”â•�â•¡ 3fded8e1-e95f-4023-b7e3-071b4d1bffd8
begin
	Base.show(io::IO, ::Type{â†’{Ï•, Ïˆ}}) where {Ï• <: Prop, Ïˆ <: Prop} = print(io, "($Ï• â†’ $Ïˆ)")
	Base.show(io::IO, ::Type{Â¬{Ï•}}) where {Ï• <: Prop} = print(io, "Â¬$Ï•")
end

# â•”â•�â•¡ a1522fde-bfc6-4419-ab54-dd475dfc3a90
begin
	abstract type ğ�’« <: Prop end
	
	abstract type P <: ğ�’« end
	abstract type Q <: ğ�’« end
end

# â•”â•�â•¡ 79fce3ea-49e0-4d2b-8db4-a7911d4fb442
abstract type Sequentce end

# â•”â•�â•¡ 36605cc1-6aca-49fc-9618-ad6b003fdeab
begin
	struct Proof{Ï•} <: Prop where {Ï• <: Prop}
		proof
	end
	
	struct MP <: Sequentce
		A::Proof
		B::Proof
	end
	
	(A::Proof{â†’{Ï•, Ïˆ}})(B::Proof{Ï•}) where {Ï• <: Prop, Ïˆ <: Prop} = Proof{Ïˆ}(MP(A, B))
	
	abstract type P1{Ï•} <: Sequentce where {Ï• <: Prop} end
	P1(::Type{Ï•}) where {Ï• <: Prop} = Proof{Ï• â†’ Ï•}(P1{Ï•})
	
	abstract type P2{Ï•, Ïˆ} <: Sequentce where {Ï• <: Prop, Ïˆ <: Prop} end
	P2(::Type{Ï•}, ::Type{Ïˆ}) where {Ï• <: Prop, Ïˆ <: Prop} = Proof{Ï• â†’ (Ïˆ â†’ Ï•)}(P2{Ï•, Ïˆ})
	
	abstract type P3{Ï•, Ïˆ, Î¶} <: Sequentce where {Ï• <: Prop, Ïˆ <: Prop, Î¶ <: Prop} end
	P3(::Type{Ï•}, ::Type{Ïˆ}, ::Type{Î¶}) where {Ï• <: Prop, Ïˆ <: Prop, Î¶ <: Prop} = Proof{(Ï• â†’ (Ïˆ â†’ Î¶)) â†’ ((Ï• â†’ Ïˆ) â†’ (Ïˆ â†’ Î¶))}(P3{Ï•, Ïˆ, Î¶})
	
	abstract type P4{Ï•, Ïˆ} <: Sequentce where {Ï• <: Prop, Ïˆ <: Prop} end
	P4(::Type{Ï•}, ::Type{Ïˆ}) where {Ï• <: Prop, Ïˆ <: Prop} = Proof{(Â¬Ï• â†’ Â¬Ïˆ) â†’ (Ïˆ â†’ Ï•)}(P4{Ï•, Ïˆ})
end

Base.show(io::IO, p::Proof{Ï•}) where {Ï• <: Prop} = print(io, "Proof : $Ï•")


# â•”â•�â•¡ 5ef40058-5ad1-4c1d-8a37-29a80ba42c08
ğ�•ƒ = (P, Q)

# â•”â•�â•¡ 1abb3647-2834-4352-a136-b34a55e43862
begin
	function Base.rand(::Type{Prop}; Ï�::Float64 = 0.6)
		if rand() â‰¤ Ï�
			rand(Bool) ? â†’{rand(Prop), rand(Prop)} : Â¬{rand(Prop)}
		else
			rand(ğ�•ƒ)
		end
	end
	
	Base.rand(::Type{P1}) = P1(rand(Prop))
	Base.rand(::Type{P2}) = P2(rand(Prop), rand(Prop))
	Base.rand(::Type{P3}) = P3(rand(Prop), rand(Prop), rand(Prop))
	Base.rand(::Type{P4}) = P4(rand(Prop), rand(Prop))
	
	Base.rand(::Type{Sequentce}) = rand(rand([P1, P2, P3, P4]))
end

# â•”â•�â•¡ 4c7cbbeb-7a2b-4256-b9d8-91e2af65ba39
Ï„ = Dict{DataType, Vector{Proof}}()
theoremcount = 0

# â•”â•�â•¡ 823bb686-8d3e-4d51-b517-6932fe7143ba
function addtheorem!(A::Proof{â†’{Ï•, Ïˆ}}; threshold = 1000) where {Ï• <: Prop, Ïˆ <: Prop}
        if theoremcount â‰¤ threshold
                haskey(Ï„, Ï•) ? nothing : Ï„[Ï•] = Proof[]	
	        A âˆˆ Ï„[Ï•] ? nothing : push!(Ï„[Ï•], A)
                global theoremcount
                theoremcount += 1
	
        	if haskey(Ï„, â†’{Ï•, Ïˆ})
	        	for p âˆˆ Ï„[â†’{Ï•, Ïˆ}]; addtheorem!(p(A); threshold = threshold); end
	        end
        end
end

# â•”â•�â•¡ f02bd8cd-f549-43b1-b5da-8f5d77d5ecb7
function generatetheorems(N = 1000; ğ�•ƒ = (P, ))
        global theoremcount
	while theoremcount â‰¤ N
		addtheorem!(rand(Sequentce); threshold = N)
	end
end

function findtheorem(::Type{â†’{Ï•, Ïˆ}}) where {Ï• <: Prop, Ïˆ  <: Prop}
    if haskey(Ï„, Ï•)
        for p âˆˆ Ï„[Ï•]
            if typeof(p) == Proof{â†’{Ï•, Ïˆ}}
                return p
            end
        end
    end
end


#
# â•”â•�â•¡ Cell order:
# â• â•�40dd03fa-bb9a-11eb-3a08-a30e7215415b
# â• â•�814f0f17-d918-4a5b-8504-4ad0f9ea25b1
# â• â•�90cecfc3-753b-4a4e-85aa-6bf8b6face58
# â• â•�035c180e-631f-4dc3-9c5e-d5fe4f0d865c
# â• â•�3fded8e1-e95f-4023-b7e3-071b4d1bffd8
# â• â•�a1522fde-bfc6-4419-ab54-dd475dfc3a90
# â• â•�79fce3ea-49e0-4d2b-8db4-a7911d4fb442
# â• â•�36605cc1-6aca-49fc-9618-ad6b003fdeab
# â• â•�5ef40058-5ad1-4c1d-8a37-29a80ba42c08
# â• â•�1abb3647-2834-4352-a136-b34a55e43862
# â• â•�4c7cbbeb-7a2b-4256-b9d8-91e2af65ba39
# â• â•�823bb686-8d3e-4d51-b517-6932fe7143ba
# â• â•�f02bd8cd-f549-43b1-b5da-8f5d77d5ecb7
