Library hydras.Ackermann.checkPrf
checkPrf.v
Original file by Russel O'Connor
From Coq Require Import Arith Lia.
From hydras.Ackermann Require Import primRec codeFreeVar
codeSubFormula cPair code folProp extEqualNat wellFormed
folProof prLogic.
From hydras Require Import Compat815.
From LibHyps Require Export LibHyps.
From hydras Require Export MoreLibHyps NewNotations.
Import LispAbbreviations.
Import FolNotations.
Section Check_Proof.
Generalizable All Variables.
Variable L : Language.
Context `(cL: Lcode L cf cr).
Variable codeArityF : nat → nat.
Variable codeArityR : nat → nat.
Context (codeArityFIsPR : isPR 1 codeArityF).
Hypothesis codeArityFIsCorrect1 :
∀ f : Functions L, codeArityF (cf f) = S (arityF L f).
Hypothesis codeArityFIsCorrect2 :
∀ n : nat, codeArityF n ≠ 0 →
∃ f : Functions L, cf f = n.
Context (codeArityRIsPR : isPR 1 codeArityR).
Hypothesis
codeArityRIsCorrect1 :
∀ r : Relations L, codeArityR (cr r) = S (arityR L r).
Hypothesis
codeArityRIsCorrect2 :
∀ n : nat, codeArityR n ≠ 0 →
∃ r : Relations L, cr r = n.
Hypothesis codeFInj : ∀ f g : Functions L,
cf f = cf g → f = g.
Hypothesis codeRInj :
∀ R S : Relations L, cr R = cr S → R = S.
Let Term := Term L.
Let Terms := Terms L.
Let Formula := Formula L.
Let wellFormedTerm := wellFormedTerm codeArityF.
Let wellFormedFormula := wellFormedFormula codeArityF codeArityR.
Let Prf := Prf L.
The wellFormedness requirement isn't really neccesary,
because any proof that used ``extra symbols'' could be
turned into a proof that only used symbols from the
axioms and the conclusion.
However making this assumption makes the proof easier
p is (cPair (formula) (proof of the Formula))
Definition checkPrfAXM (p recs : nat) :=
switchPR (charFunction 2 Nat.eqb (cddr p) (car p))
(S (S (cPair (car p) 0))) 0.
#[export] Instance checkPrfAXMIsPR : isPR 2 checkPrfAXM.
Definition checkPrfMP (p recs : nat) :=
switchPR
(wellFormedFormula (car (cdr (cdr (cdr p)))) ×
(charFunction 2 Nat.eqb (car (car (cdr (cdr p))))
(codeImp (car (cdr (cdr (cdr p)))) (car p)) ×
(codeNth (p - S (caddr p)) recs ×
codeNth (p - S (cdddr p)) recs)))
(S
(codeApp
(pred (codeNth (p - S (caddr p)) recs))
(pred (codeNth (p - S (cdr (cdr (cdr p)))) recs))))
0.
#[export] Instance checkPrfMPIsPR : isPR 2 checkPrfMP.
Definition checkPrfGEN (p recs : nat) :=
switchPR
(charFunction 2 Nat.eqb
(cPair 3
(cPair (car (cdr (cdr p)))
(car (cdr (cdr (cdr p))))))
(car p) ×
(codeNth (p - S (cdr (cdr (cdr p)))) recs ×
(1 -
codeIn (car (cdr (cdr p)))
(codeFreeVarListFormula
(pred (codeNth (p - S (cdr (cdr (cdr p)))) recs))))))
(codeNth (p - S (cdr (cdr (cdr p)))) recs) 0.
#[export] Instance checkPrfGENIsPR : isPR 2 checkPrfGEN.
Definition checkPrfIMP1 (p recs : nat) :=
let A := car (cdr (cdr p)) in
let B := cdr (cdr (cdr p)) in
charFunction 2 Nat.eqb (cPair 1 (cPair A (cPair 1 (cPair B A))))
(car p).
#[export] Instance checkPrfIMP1IsPR : isPR 2 checkPrfIMP1.
Definition checkPrfIMP2 (p recs : nat) :=
let A := car (cdr (cdr p)) in
let B := car (cdr (cdr (cdr p))) in
let C := cdr (cdr (cdr (cdr p))) in
charFunction 2 Nat.eqb
(cPair 1
(cPair (cPair 1 (cPair A (cPair 1 (cPair B C))))
(cPair 1 (cPair (cPair 1 (cPair A B)) (cPair 1 (cPair A C))))))
(car p).
#[export] Instance checkPrfIMP2IsPR : isPR 2 checkPrfIMP2.
Definition checkPrfCP (p recs : nat) :=
let A := car (cdr (cdr p)) in
let B := cdr (cdr (cdr p)) in
charFunction 2 Nat.eqb
(cPair 1
(cPair (cPair 1 (cPair (cPair 2 A) (cPair 2 B))) (cPair 1 (cPair B A))))
(car p).
#[export] Instance checkPrfCPIsPR : isPR 2 checkPrfCP.
Definition checkPrfFA1 (p recs : nat) :=
let A := car (cdr (cdr p)) in
let v := car (cdr (cdr (cdr p))) in
let t := cdr (cdr (cdr (cdr p))) in
wellFormedTerm t ×
charFunction 2 Nat.eqb
(cPair 1 (cPair (cPair 3 (cPair v A)) (codeSubFormula A v t)))
(car p).
#[export] Instance checkPrfFA1IsPR : isPR 2 checkPrfFA1.
Definition checkPrfFA2 (p recs : nat) :=
let A := car (cdr (cdr p)) in
let v := cdr (cdr (cdr p)) in
(1 - codeIn v (codeFreeVarFormula A)) ×
charFunction 2 Nat.eqb (cPair 1 (cPair A (cPair 3 (cPair v A))))
(car p).
#[export] Instance checkPrfFA2IsPR : isPR 2 checkPrfFA2.
Definition checkPrfFA3 (p recs : nat) :=
let A := car (cdr (cdr p)) in
let B := car (cdr (cdr (cdr p))) in
let v := cdr (cdr (cdr (cdr p))) in
charFunction 2 Nat.eqb
(cPair 1
(cPair (cPair 3 (cPair v (cPair 1 (cPair A B))))
(cPair 1 (cPair (cPair 3 (cPair v A)) (cPair 3 (cPair v B))))))
(car p).
#[export] Instance checkPrfFA3IsPR : isPR 2 checkPrfFA3.
Definition checkPrfEQ1 (p recs : nat) :=
charFunction 2 Nat.eqb (cdr (cdr p)) 0 ×
charFunction 2 Nat.eqb
(codeFormula (equal (var 0) (var 0)))
(car p).
Lemma checkPrfEQnIsPR (n: nat):
isPR 2
(fun p recs : nat ⇒
charFunction 2 Nat.eqb (cdr (cdr p)) 0 ×
charFunction 2 Nat.eqb n (car p)).
#[export] Instance checkPrfEQ1IsPR : isPR 2 checkPrfEQ1.
Definition checkPrfEQ2 (p recs : nat) :=
charFunction 2 Nat.eqb (cdr (cdr p)) 0 ×
charFunction 2 Nat.eqb
(codeFormula (v#0 = v#1 → v#1 = v#0)%fol) (car p).
#[export] Instance checkPrfEQ2IsPR : isPR 2 checkPrfEQ2.
Definition checkPrfEQ3 (p recs : nat) :=
charFunction 2 Nat.eqb (cdr (cdr p)) 0 ×
charFunction 2 Nat.eqb
(codeFormula
(v#0 = v#1 → v#1 = v#2 → v#0 = v#2)%fol)
(car p).
#[export] Instance checkPrfEQ3IsPR : isPR 2 checkPrfEQ3.
Definition codeAxmEqHelp (n f : nat) : nat :=
nat_rec (fun _ ⇒ nat) f
(fun m rec : nat ⇒
cPair 1
(cPair (cPair 0 (cPair (cPair 0 (m + m)) (cPair 0 (S (m + m))))) rec))
n.
#[export] Instance codeAxmEqHelpIsPR : isPR 2 codeAxmEqHelp.
Definition codeNVars1 (n : nat) : nat :=
nat_rec (fun _ ⇒ nat) 0
(fun m rec : nat ⇒ S (cPair (cPair 0 (m + m)) rec)) n.
#[export] Instance codeNVars1IsPR : isPR 1 codeNVars1.
Definition codeNVars2 (n : nat) : nat :=
nat_rec (fun _ ⇒ nat) 0
(fun m rec : nat ⇒ S (cPair (cPair 0 (S (m + m))) rec)) n.
#[export] Instance codeNVars2IsPR : isPR 1 codeNVars2.
Lemma codeNVarsCorrect (n: nat) :
codeNVars1 n = codeTerms (fst (nVars L n)) ∧
codeNVars2 n = codeTerms (snd (nVars L n)).
Definition checkPrfEQ4 (p recs : nat) :=
let r := cdr (cdr p) in
let A := cPair (S (S (S (S r)))) (codeNVars1 (pred (codeArityR r))) in
let B := cPair (S (S (S (S r)))) (codeNVars2 (pred (codeArityR r))) in
notZero (codeArityR r) ×
charFunction 2 Nat.eqb (codeAxmEqHelp (pred (codeArityR r)) (codeIff A B))
(car p).
#[export] Instance codeOrIsPR : isPR 2 codeOr.
#[export] Instance codeAndIsPR : isPR 2 codeAnd.
#[export] Instance codeIffIsPR : isPR 2 codeIff.
#[export] Instance checkPrfEQ4IsPR : isPR 2 checkPrfEQ4.
Definition checkPrfEQ5 (p recs : nat) :=
let f := cdr (cdr p) in
notZero (codeArityF f) ×
charFunction 2 Nat.eqb
(codeAxmEqHelp (pred (codeArityF f))
(cPair 0
(cPair (cPair (S f) (codeNVars1 (pred (codeArityF f))))
(cPair (S f) (codeNVars2 (pred (codeArityF f)))))))
(car p).
#[export] Instance checkPrfEQ5IsPR : isPR 2 checkPrfEQ5.
Definition checkPrfHelp : nat → nat :=
evalStrongRec 0
(fun p recs : nat ⇒
let type := car (cdr p) in
switchPR type
(switchPR (pred type)
(switchPR (pred (pred type))
(switchPR (pred (pred (pred type)))
(switchPR (pred (pred (pred (pred type))))
(switchPR (pred (pred (pred (pred (pred type)))))
(switchPR
(pred (pred (pred (pred (pred (pred type))))))
(switchPR
(pred
(pred (pred (pred (pred (pred (pred type)))))))
(switchPR
(pred
(pred
(pred
(pred
(pred (pred (pred (pred type))))))))
(switchPR
(pred
(pred
(pred
(pred
(pred
(pred
(pred (pred (pred type)))))))))
(switchPR
(pred
(pred
(pred
(pred
(pred
(pred
(pred
(pred
(pred (pred type))))))))))
(switchPR
(pred
(pred
(pred
(pred
(pred
(pred
(pred
(pred
(pred
(pred (pred type)))))))))))
(switchPR
(pred
(pred
(pred
(pred
(pred
(pred
(pred
(pred
(pred
(pred (pred (pred type))))))))))))
(switchPR
(pred
(pred
(pred
(pred
(pred
(pred
(pred
(pred
(pred
(pred
(pred (pred (pred type)))))))))))))
0 (checkPrfEQ5 p recs))
(checkPrfEQ4 p recs))
(checkPrfEQ3 p recs))
(checkPrfEQ2 p recs))
(checkPrfEQ1 p recs))
(checkPrfFA3 p recs))
(checkPrfFA2 p recs)) (checkPrfFA1 p recs))
(checkPrfCP p recs)) (checkPrfIMP2 p recs))
(checkPrfIMP1 p recs)) (checkPrfGEN p recs))
(checkPrfMP p recs)) (checkPrfAXM p recs)).
#[local] Instance checkPrfHelpIsPR : isPR 1 checkPrfHelp.
Definition checkPrf (f p : nat) : nat :=
switchPR (wellFormedFormula f) (checkPrfHelp (cPair f p)) 0.
#[export] Instance checkPrfIsPR : isPR 2 checkPrf.
Lemma checkPrfCorrect1 (l : list Formula) (f : Formula) (p : Prf l f):
checkPrf (codeFormula f) (codePrf l f p)
= S (codeList (map codeFormula l)).
Lemma checkPrfCorrect2 (n m : nat):
checkPrf n m ≠ 0 →
∃ f : Formula,
codeFormula f = n ∧
(∃ l : list Formula,
(∃ p : Prf l f, codePrf l f p = m)).
End Check_Proof.
Arguments codePrf {L cf cr cl} _.