loa

2023-11-22-declare-prove-use.lua (3673B)

---

 local pprint = require("pprint").pprint
 -- Possible actions:
 -- * start subcontext
 -- * declare judgment
 -- * use declared judgment
 
 function die(err, msg, ...)
 	msg = tostring(msg or err)
 	if err then
 		io.stderr:write(string.format(msg .. "\n", ...))
 		os.exit(1)
 	end
 end
 
 local test = {
 	{
 		method = "down"
 	},
 	{
 		method = "declare",
 		params = {
 			name = "cv",
 			judgment = {
 				head = "var",
 				body = {
 					{
 						head = "x"
 					}
 				}
 			}
 		}
 	},
 	{
 		method = "up"
 	},
 	{
 		method = "declare",
 		params = {
 			name = "var-wff",
 			judgment = {
 				head = "wff",
 				body = {
 					{
 						head = "x"
 					}
 				}
 			}
 		}
 	}
 }
 
 local actions = {}
 
 function actions.down(state)
 	die(state.subcontext, "Unresolved subcontext")
 	table.insert(state.theories, {})
 	return state
 end
 
 function actions.up(state)
 	state.subcontext = state.theories[#state.theories]
 	table.remove(state.theories)
 	return state
 end
 
 function pressupositions(state, judgment)
 	-- This is a rabbit hole. Where do pressupositions come from? Two
 	-- options: 1) we fix the forms of judgments and hard-code the
 	-- pressupositions; 2) we find a way for the user to create
 	-- *declaration rules* that work just like assumptions but are
 	-- only used at top-level declarations.
 	return {}
 end
 
 function actions.declare(state, params)
 	die(state.focus, "Proof in progress")
 	local assumption = {
 		name = params.name,
 		conclusion = params.judgment,
 		subcontext = state.subcontext
 	}
 	state.subcontext = nil
 	table.insert(state.theories[#state.theories], assumption)
 	state.goals = pressupositions(state, params.judgment)
 	return state
 end
 
 function prune(state)
 	while #state.focus.subgoals == 0 do
  		die(not match(state.focus.goal, state.focus.candidate), "Used assumption does not prove the goal")
 		if state.focus.goal.head == "var" then
 			-- oh boy
 			-- perform unifications
 		end
 		if state.focus.parent then
 			state.focus = state.focus.parent
 			table.remove(state.focus.subgoals)
 		else
 			table.remove(state.goals)
 			if #state.goals > 0 then
 				state.focus = state.goals[#state.goals]
 			else
 				state.focus = nil
 			end
 			return state
 		end
 	end
 	return state
 end
 
 function use(state, assumption)
 	state.focus.candidate = assumption.conclusion
 	if #assumption.subcontext > 0 then
 		for i = #candidate.subcontext, 1, -1 do
 			table.insert(state.focus.subgoals, candidate.subcontext[i])
 			state.focus.subgoals[i].parent = state.focus
 		end
 		state.focus = state.focus.subgoals[#state.focus.subgoals]
 	end
 end
 
 function actions.use(state, name)
 	die(not state.goals.focus, "Nothing to prove")
 
 	local assumption = state.assets[name]
 	die(not assumption, "No assumption under that name")
 	state = use(state, assumption)
 	state = prune(state)
 	return state
 end
 
 function interpret(program, state)
 	for _,c in ipairs(program) do
 		die(not actions[c.method], "No such action '%s'", c.method)
 		state = actions[c.method](state, c.params)
 	end
 	return state
 end
 
 function judgment2str(judg)
 	local res = judg.head
 	if judg.body then
 		res = res .. "("
 		for i = 1, #judg.body do
 			res = res .. judgment2str(judg.body[i])
 			if i < #judg.body then
 				res = res .. ","
 			end
 		end
 		res = res .. ")"
 	end
 	return res
 end
 
 function printassumption(assump, level)
 	if assump.subcontext then
 		printtheory(assump.subcontext, level + 1)
 	end
 	io.write(string.rep(" ", level) .. assump.name .. " " .. judgment2str(assump.conclusion) .. "\n")
 end
 
 function printtheory(th, level)
 	level = level or 0
 	for _,a in ipairs(th) do
 		printassumption(a, level)
 	end
 end
 
 local init = {
 	goals = {},
 	theories = {{}}
 }
 
 local bigres = interpret(test, init)
 printtheory(bigres.theories[1])