Skip to content

Instantly share code, notes, and snippets.

@palmskog

palmskog/fitch.cml

Last active May 9, 2021 05:28
Show Gist options
  • Save palmskog/a988783a000ae6319eed15819eeb60ac to your computer and use it in GitHub Desktop.
Save palmskog/a988783a000ae6319eed15819eeb60ac to your computer and use it in GitHub Desktop.
Download ZIP
Verified Fitch-style proof checker in CakeML - "make fitch.cake" to compile with the bootstrapped compiler
Raw
fitch.cml
fun valid_derivation_deriv_premise_cake v2 =
(fn v1 => List.member v1 v2);
datatype fitch_prop = Prop_cont
| Prop_imp (fitch_prop) (fitch_prop)
| Prop_or (fitch_prop) (fitch_prop)
| Prop_and (fitch_prop) (fitch_prop)
| Prop_neg (fitch_prop)
| Prop_p (char list);
fun valid_derivation_deriv_lem_cake v17 =
case v17
of (Prop_p (v1)) => (0 < 0)
| (Prop_neg (v2)) => (0 < 0)
| (Prop_and (v4) (v3)) => (0 < 0)
| (Prop_or (v14) (v13)) => (case v13
of ((Prop_p (v5))) => (0 < 0)
| ((Prop_neg (v6))) => (v14 = v6)
| ((Prop_and (v8) (v7))) => (0 < 0)
| ((Prop_or (v10) (v9))) => (0 < 0)
| ((Prop_imp (v12) (v11))) => (0 < 0)
| Prop_cont => (0 < 0))
| (Prop_imp (v16) (v15)) => (0 < 0)
| Prop_cont => (0 < 0);
fun valid_derivation_deriv_copy_cake v6 =
(fn v4 =>
(fn v5 =>
case (Map.lookup v6 ((Inl (v4))))
of None => (0 < 0)
| (Some (v3)) => (case v3
of ((Inl (v1))) => (v5 = v1)
| ((Inr (v2))) => (0 < 0))));
fun valid_derivation_deriv_andi_cake v7 =
(fn v8 =>
(fn v9 =>
(fn v10 =>
case (Map.lookup v7 ((Inl (v8))))
of None => (0 < 0)
| (Some (v6)) => (case v6
of ((Inl (v4))) => (case (Map.lookup v7 ((Inl (v9))))
of None => (0 < 0)
| ((Some (v3))) => (case v3
of ((Inl (v1))) => (v10 = ((Prop_and (v4) (v1))))
| ((Inr (v2))) => (0 < 0)))
| ((Inr (v5))) => (0 < 0)))));
fun valid_derivation_deriv_ande1_cake v14 =
(fn v12 =>
(fn v13 =>
case (Map.lookup v14 ((Inl (v12))))
of None => (0 < 0)
| (Some (v11)) => (case v11
of ((Inl (v9))) => (case v9
of ((Prop_p (v1))) => (0 < 0)
| ((Prop_neg (v2))) => (0 < 0)
| ((Prop_and (v4) (v3))) => (v13 = v4)
| ((Prop_or (v6) (v5))) => (0 < 0)
| ((Prop_imp (v8) (v7))) => (0 < 0)
| Prop_cont => (0 < 0))
| ((Inr (v10))) => (0 < 0))));
fun valid_derivation_deriv_ande2_cake v14 =
(fn v12 =>
(fn v13 =>
case (Map.lookup v14 ((Inl (v12))))
of None => (0 < 0)
| (Some (v11)) => (case v11
of ((Inl (v9))) => (case v9
of ((Prop_p (v1))) => (0 < 0)
| ((Prop_neg (v2))) => (0 < 0)
| ((Prop_and (v4) (v3))) => (v13 = v3)
| ((Prop_or (v6) (v5))) => (0 < 0)
| ((Prop_imp (v8) (v7))) => (0 < 0)
| Prop_cont => (0 < 0))
| ((Inr (v10))) => (0 < 0))));
fun valid_derivation_deriv_ori1_cake v14 =
(fn v12 =>
(fn v13 =>
case v13
of (Prop_p (v1)) => (0 < 0)
| (Prop_neg (v2)) => (0 < 0)
| (Prop_and (v4) (v3)) => (0 < 0)
| (Prop_or (v9) (v8)) => (case (Map.lookup v14 ((Inl (v12))))
of None => (0 < 0)
| ((Some (v7))) => (case v7
of ((Inl (v5))) => (v9 = v5)
| ((Inr (v6))) => (0 < 0)))
| (Prop_imp (v11) (v10)) => (0 < 0)
| Prop_cont => (0 < 0)));
fun valid_derivation_deriv_ori2_cake v14 =
(fn v12 =>
(fn v13 =>
case v13
of (Prop_p (v1)) => (0 < 0)
| (Prop_neg (v2)) => (0 < 0)
| (Prop_and (v4) (v3)) => (0 < 0)
| (Prop_or (v9) (v8)) => (case (Map.lookup v14 ((Inl (v12))))
of None => (0 < 0)
| ((Some (v7))) => (case v7
of ((Inl (v5))) => (v8 = v5)
| ((Inr (v6))) => (0 < 0)))
| (Prop_imp (v11) (v10)) => (0 < 0)
| Prop_cont => (0 < 0)));
fun valid_derivation_deriv_impe_cake v18 =
(fn v15 =>
(fn v16 =>
(fn v17 =>
case (Map.lookup v18 ((Inl (v15))))
of None => (0 < 0)
| (Some (v14)) => (case v14
of ((Inl (v12))) => (case (Map.lookup v18 ((Inl (v16))))
of None => (0 < 0)
| ((Some (v11))) => (case v11
of ((Inl (v9))) => (case v9
of ((Prop_p (v1))) => (0 < 0)
| ((Prop_neg (v2))) => (0 < 0)
| ((Prop_and (v4) (v3))) => (0 < 0)
| ((Prop_or (v6) (v5))) => (0 < 0)
| ((Prop_imp (v8) (v7))) => ((v12 = v8) andalso (v17 = v7))
| Prop_cont => (0 < 0))
| ((Inr (v10))) => (0 < 0)))
| ((Inr (v13))) => (0 < 0)))));
fun valid_derivation_deriv_nege_cake v26 =
(fn v23 =>
(fn v24 =>
(fn v25 =>
case v25
of (Prop_p (v1)) => (0 < 0)
| (Prop_neg (v2)) => (0 < 0)
| (Prop_and (v4) (v3)) => (0 < 0)
| (Prop_or (v6) (v5)) => (0 < 0)
| (Prop_imp (v8) (v7)) => (0 < 0)
| Prop_cont => (case (Map.lookup v26 ((Inl (v23))))
of None => (0 < 0)
| ((Some (v22))) => (case v22
of ((Inl (v20))) => (case (Map.lookup v26 ((Inl (v24))))
of None => (0 < 0)
| ((Some (v19))) => (case v19
of ((Inl (v17))) => (case v17
of ((Prop_p (v9))) => (0 < 0)
| ((Prop_neg (v10))) => (v20 = v10)
| ((Prop_and (v12) (v11))) => (0 < 0)
| ((Prop_or (v14) (v13))) => (0 < 0)
| ((Prop_imp (v16) (v15))) => (0 < 0)
| Prop_cont => (0 < 0))
| ((Inr (v18))) => (0 < 0)))
| ((Inr (v21))) => (0 < 0))))));
fun valid_derivation_deriv_conte_cake v13 =
(fn v12 =>
case (Map.lookup v13 ((Inl (v12))))
of None => (0 < 0)
| (Some (v11)) => (case v11
of ((Inl (v9))) => (case v9
of ((Prop_p (v1))) => (0 < 0)
| ((Prop_neg (v2))) => (0 < 0)
| ((Prop_and (v4) (v3))) => (0 < 0)
| ((Prop_or (v6) (v5))) => (0 < 0)
| ((Prop_imp (v8) (v7))) => (0 < 0)
| Prop_cont => (0 <= 0))
| ((Inr (v10))) => (0 < 0)));
fun valid_derivation_deriv_negnegi_cake v22 =
(fn v20 =>
(fn v21 =>
case v21
of (Prop_p (v1)) => (0 < 0)
| (Prop_neg (v13)) => (case v13
of ((Prop_p (v2))) => (0 < 0)
| ((Prop_neg (v6))) => (case (Map.lookup v22 ((Inl (v20))))
of None => (0 < 0)
| ((Some (v5))) => (case v5
of ((Inl (v3))) => (v6 = v3)
| ((Inr (v4))) => (0 < 0)))
| ((Prop_and (v8) (v7))) => (0 < 0)
| ((Prop_or (v10) (v9))) => (0 < 0)
| ((Prop_imp (v12) (v11))) => (0 < 0)
| Prop_cont => (0 < 0))
| (Prop_and (v15) (v14)) => (0 < 0)
| (Prop_or (v17) (v16)) => (0 < 0)
| (Prop_imp (v19) (v18)) => (0 < 0)
| Prop_cont => (0 < 0)));
fun valid_derivation_deriv_negnege_cake v22 =
(fn v20 =>
(fn v21 =>
case (Map.lookup v22 ((Inl (v20))))
of None => (0 < 0)
| (Some (v19)) => (case v19
of ((Inl (v17))) => (case v17
of ((Prop_p (v1))) => (0 < 0)
| ((Prop_neg (v10))) => (case v10
of ((Prop_p (v2))) => (0 < 0)
| ((Prop_neg (v3))) => (v3 = v21)
| ((Prop_and (v5) (v4))) => (0 < 0)
| ((Prop_or (v7) (v6))) => (0 < 0)
| ((Prop_imp (v9) (v8))) => (0 < 0)
| Prop_cont => (0 < 0))
| ((Prop_and (v12) (v11))) => (0 < 0)
| ((Prop_or (v14) (v13))) => (0 < 0)
| ((Prop_imp (v16) (v15))) => (0 < 0)
| Prop_cont => (0 < 0))
| ((Inr (v18))) => (0 < 0))));
fun valid_derivation_deriv_mt_cake v34 =
(fn v31 =>
(fn v32 =>
(fn v33 =>
case v33
of (Prop_p (v1)) => (0 < 0)
| (Prop_neg (v24)) => (case (Map.lookup v34 ((Inl (v31))))
of None => (0 < 0)
| ((Some (v23))) => (case v23
of ((Inl (v21))) => (case v21
of ((Prop_p (v2))) => (0 < 0)
| ((Prop_neg (v3))) => (0 < 0)
| ((Prop_and (v5) (v4))) => (0 < 0)
| ((Prop_or (v7) (v6))) => (0 < 0)
| ((Prop_imp (v20) (v19))) => (if (v24 = v20)
then (case (Map.lookup v34 ((Inl (v32))))
of None => (0 < 0)
| ((Some (v18))) => (case v18
of ((Inl (v16))) => (case v16
of ((Prop_p (v8))) => (0 < 0)
| ((Prop_neg (v9))) => (v19 = v9)
| ((Prop_and (v11) (v10))) => (0 < 0)
| ((Prop_or (v13) (v12))) => (0 < 0)
| ((Prop_imp (v15) (v14))) => (0 < 0)
| Prop_cont => (0 < 0))
| ((Inr (v17))) => (0 < 0)))
else (0 < 0))
| Prop_cont => (0 < 0))
| ((Inr (v22))) => (0 < 0)))
| (Prop_and (v26) (v25)) => (0 < 0)
| (Prop_or (v28) (v27)) => (0 < 0)
| (Prop_imp (v30) (v29)) => (0 < 0)
| Prop_cont => (0 < 0))));
fun valid_derivation_deriv_impi_cake v17 =
(fn v14 =>
(fn v15 =>
(fn v16 =>
case v16
of (Prop_p (v1)) => (0 < 0)
| (Prop_neg (v2)) => (0 < 0)
| (Prop_and (v4) (v3)) => (0 < 0)
| (Prop_or (v6) (v5)) => (0 < 0)
| (Prop_imp (v13) (v12)) => (case (Map.lookup v17 (let val x =
(v14,v15)
in
(Inr (x))
end))
of None => (0 < 0)
| ((Some (v11))) => (case v11
of ((Inl (v7))) => (0 < 0)
| ((Inr (v10))) => (case v10
of (v9,v8) => ((v13 = v9) andalso (v12 = v8)))))
| Prop_cont => (0 < 0))));
fun valid_derivation_deriv_negi_cake v25 =
(fn v22 =>
(fn v23 =>
(fn v24 =>
case v24
of (Prop_p (v1)) => (0 < 0)
| (Prop_neg (v15)) => (case (Map.lookup v25 (let val x =
(v22,v23)
in
(Inr (x))
end))
of None => (0 < 0)
| ((Some (v14))) => (case v14
of ((Inl (v2))) => (0 < 0)
| ((Inr (v13))) => (case v13
of (v12,v11) => (case v11
of ((Prop_p (v3))) => (0 < 0)
| ((Prop_neg (v4))) => (0 < 0)
| ((Prop_and (v6) (v5))) => (0 < 0)
| ((Prop_or (v8) (v7))) => (0 < 0)
| ((Prop_imp (v10) (v9))) => (0 < 0)
| Prop_cont => (v15 = v12)))))
| (Prop_and (v17) (v16)) => (0 < 0)
| (Prop_or (v19) (v18)) => (0 < 0)
| (Prop_imp (v21) (v20)) => (0 < 0)
| Prop_cont => (0 < 0))));
fun valid_derivation_deriv_ore_cake v28 =
(fn v22 =>
(fn v23 =>
(fn v24 =>
(fn v25 =>
(fn v26 =>
(fn v27 =>
case (Map.lookup v28 ((Inl (v22))))
of None => (0 < 0)
| (Some (v21)) => (case v21
of ((Inl (v19))) => (case v19
of ((Prop_p (v1))) => (0 < 0)
| ((Prop_neg (v2))) => (0 < 0)
| ((Prop_and (v4) (v3))) => (0 < 0)
| ((Prop_or (v16) (v15))) => (case (Map.lookup v28 (let val x =
(v23,v24)
in
(Inr (x))
end))
of None => (0 < 0)
| ((Some (v14))) => (case v14
of ((Inl (v5))) => (0 < 0)
| ((Inr (v13))) => (case v13
of (v12,v11) => (if ((v16 = v12) andalso (v27 = v11))
then (case (Map.lookup v28 (let val x = (v25,v26)
in
(Inr (x))
end))
of None => (0 < 0)
| ((Some (v10))) => (case v10
of ((Inl (v6))) => (0 < 0)
| ((Inr (v9))) => (case v9
of (v8,v7) => ((v15 = v8) andalso (v27 = v7)))))
else (0 < 0)))))
| ((Prop_imp (v18) (v17))) => (0 < 0)
| Prop_cont => (0 < 0))
| ((Inr (v20))) => (0 < 0))))))));
fun valid_derivation_deriv_pbc_cake v25 =
(fn v22 =>
(fn v23 =>
(fn v24 =>
case (Map.lookup v25 (let val x = (v22,v23)
in
(Inr (x))
end))
of None => (0 < 0)
| (Some (v21)) => (case v21
of ((Inl (v1))) => (0 < 0)
| ((Inr (v20))) => (case v20
of (v19,v18) => (case v19
of ((Prop_p (v2))) => (0 < 0)
| ((Prop_neg (v11))) => (case v18
of ((Prop_p (v3))) => (0 < 0)
| ((Prop_neg (v4))) => (0 < 0)
| ((Prop_and (v6) (v5))) => (0 < 0)
| ((Prop_or (v8) (v7))) => (0 < 0)
| ((Prop_imp (v10) (v9))) => (0 < 0)
| Prop_cont => (v11 = v24))
| ((Prop_and (v13) (v12))) => (0 < 0)
| ((Prop_or (v15) (v14))) => (0 < 0)
| ((Prop_imp (v17) (v16))) => (0 < 0)
| Prop_cont => (0 < 0)))))));
datatype fitch_justification = Justification_pbc (int) (int)
| Justification_ore (int) (int) (int) (int) (int)
| Justification_negi (int) (int)
| Justification_impi (int) (int)
| Justification_mt (int) (int)
| Justification_negnege (int)
| Justification_negnegi (int)
| Justification_conte (int)
| Justification_nege (int) (int)
| Justification_impe (int) (int)
| Justification_ori2 (int)
| Justification_ori1 (int)
| Justification_ande2 (int)
| Justification_ande1 (int)
| Justification_andi (int) (int)
| Justification_copy (int)
| Justification_lem
| Justification_premise;
datatype fitch_reason = Reason_justification (fitch_justification)
| Reason_assumption;
fun valid_derivation_deriv_cake v32 =
(fn v30 =>
(fn v29 =>
(fn v31 =>
case v31
of Reason_assumption => (0 < 0)
| (Reason_justification (v28)) => (case v28
of Justification_premise => (valid_derivation_deriv_premise_cake v30 v29)
| Justification_lem => (valid_derivation_deriv_lem_cake v29)
| ((Justification_copy (v1))) => (valid_derivation_deriv_copy_cake v32 v1 v29)
| ((Justification_andi (v3) (v2))) => (valid_derivation_deriv_andi_cake v32 v3 v2 v29)
| ((Justification_ande1 (v4))) => (valid_derivation_deriv_ande1_cake v32 v4 v29)
| ((Justification_ande2 (v5))) => (valid_derivation_deriv_ande2_cake v32 v5 v29)
| ((Justification_ori1 (v6))) => (valid_derivation_deriv_ori1_cake v32 v6 v29)
| ((Justification_ori2 (v7))) => (valid_derivation_deriv_ori2_cake v32 v7 v29)
| ((Justification_impe (v9) (v8))) => (valid_derivation_deriv_impe_cake v32 v9 v8 v29)
| ((Justification_nege (v11) (v10))) => (valid_derivation_deriv_nege_cake v32 v11 v10 v29)
| ((Justification_conte (v12))) => (valid_derivation_deriv_conte_cake v32 v12)
| ((Justification_negnegi (v13))) => (valid_derivation_deriv_negnegi_cake v32 v13 v29)
| ((Justification_negnege (v14))) => (valid_derivation_deriv_negnege_cake v32 v14 v29)
| ((Justification_mt (v16) (v15))) => (valid_derivation_deriv_mt_cake v32 v16 v15 v29)
| ((Justification_impi (v18) (v17))) => (valid_derivation_deriv_impi_cake v32 v18 v17 v29)
| ((Justification_negi (v20) (v19))) => (valid_derivation_deriv_negi_cake v32 v20 v19 v29)
| ((Justification_ore (v25) (v24) (v23) (v22) (v21))) => (valid_derivation_deriv_ore_cake v32 v25 v24 v23 v22 v21 v29)
| ((Justification_pbc (v27) (v26))) => (valid_derivation_deriv_pbc_cake v32 v27 v26 v29)))));
fun last_default v4 =
(fn v3 =>
case v4
of [] => v3
| v2::v1 => (List.last (v2::v1)));
datatype fitch_derivation = Derivation_deriv (int) (fitch_prop) (fitch_reason);
datatype fitch_entry = Entry_invalid
| Entry_box (fitch_entry list)
| Entry_derivation (fitch_derivation);
fun valid_proof_entry_list_cake v22 v23 v24 =
case v22
of [] => (0 <= 0)
| v21::v20 => (case v21
of ((Entry_derivation (v5))) => (case v5
of ((Derivation_deriv (v4) (v3) (v2))) => (case v2
of Reason_assumption => (0 < 0)
| ((Reason_justification (v1))) => (if (valid_entry_dec_cake v23 v24 v21)
then (valid_proof_entry_list_cake v20 (Map.insert v23 ((Inl (v4))) ((Inl (v3)))) v24)
else (0 < 0))))
| ((Entry_box (v19))) => (case v19
of [] => (0 < 0)
| (v18::v17) => (case v18
of ((Entry_derivation (v15))) => (case v15
of ((Derivation_deriv (v14) (v13) (v12))) => (case v12
of Reason_assumption => (case (last_default v19 Entry_invalid)
of ((Entry_derivation (v9))) => (case v9
of ((Derivation_deriv (v8) (v7) (v6))) => (if (valid_entry_dec_cake v23 v24 v21)
then (valid_proof_entry_list_cake v20 (Map.insert v23 (let val x = (v14,v8)
in
(Inr (x))
end) (let val x = (v13,v7)
in
(Inr (x))
end)) v24)
else (0 < 0)))
| ((Entry_box (v10))) => (0 < 0)
| Entry_invalid => (0 < 0))
| ((Reason_justification (v11))) => (0 < 0)))
| ((Entry_box (v16))) => (0 < 0)
| Entry_invalid => (0 < 0)))
| Entry_invalid => (0 < 0))
and valid_entry_dec_cake v15 v16 v17 =
case v17
of (Entry_derivation (v5)) => (case v5
of ((Derivation_deriv (v4) (v3) (v2))) => (case v2
of Reason_assumption => (0 < 0)
| ((Reason_justification (v1))) => (valid_derivation_deriv_cake v15 v16 v3 v2)))
| (Entry_box (v14)) => (case v14
of [] => (0 < 0)
| (v13::v12) => (case v13
of ((Entry_derivation (v10))) => (case v10
of ((Derivation_deriv (v9) (v8) (v7))) => (case v7
of Reason_assumption => (valid_proof_entry_list_cake v12 (Map.insert v15 ((Inl (v9))) ((Inl (v8)))) v16)
| ((Reason_justification (v6))) => (0 < 0)))
| ((Entry_box (v11))) => (0 < 0)
| Entry_invalid => (0 < 0)))
| Entry_invalid => (0 < 0);
fun valid_proof_dec_cake v3 =
(fn v1 => (fn v2 => valid_proof_entry_list_cake v2 v3 v1));
datatype fitch_judgment = Judgment_follows (fitch_prop list) (fitch_prop);
datatype fitch_claim = Claim_judgment_proof (fitch_judgment) (fitch_entry list);
fun valid_claim_dec_cmp_cake v12 =
(fn v11 =>
case v11
of (Claim_judgment_proof (v10) (v9)) => (case v10
of ((Judgment_follows (v8) (v7))) => (case (last_default v9 Entry_invalid)
of ((Entry_derivation (v5))) => (case v5
of ((Derivation_deriv (v4) (v3) (v2))) => (case v2
of Reason_assumption => (0 < 0)
| ((Reason_justification (v1))) => (if (v7 = v3)
then (valid_proof_dec_cake (Map.empty v12) v8 v9)
else (0 < 0))))
| ((Entry_box (v6))) => (0 < 0)
| Entry_invalid => (0 < 0))));
fun dyadic_cmp v13 =
(fn v12 =>
(fn v11 =>
case v12
of (Inl (v3)) => (case v11
of ((Inl (v1))) => (case (v13 v3 v1)
of Less => Less
| Equal => Equal
| Greater => Greater)
| ((Inr (v2))) => Less)
| (Inr (v10)) => (case v11
of ((Inl (v4))) => Greater
| ((Inr (v9))) => (case v9
of (v8,v7) => (case v10
of (v6,v5) => (case (v13 v6 v8)
of Less => Less
| Equal => (case (v13 v5 v7)
of Less => Less
| Equal => Equal
| Greater => Greater)
| Greater => Greater))))));
fun num_compare v1 =
(fn v2 =>
if (v1 = v2)
then Equal
else (if (v1 < v2)
then Less
else Greater));
fun dyadic_cmp_num v1 = dyadic_cmp num_compare v1;
fun valid_claim_dec_cake v1 =
valid_claim_dec_cmp_cake dyadic_cmp_num v1;
val example_premises = (Prop_p (#"p"::[] ))::(Prop_p (#"q"::[] ))::[] ;
val example_proof =
(Entry_derivation ((Derivation_deriv (1) ((Prop_p (#"p"::[] ))) ((Reason_justification (Justification_premise))))))::(Entry_derivation ((Derivation_deriv (2) ((Prop_p (#"q"::[] ))) ((Reason_justification (Justification_premise))))))::(Entry_derivation ((Derivation_deriv (3) ((Prop_and ((Prop_p (#"p"::[] ))) ((Prop_p (#"q"::[] ))))) ((Reason_justification ((Justification_andi (1) (2))))))))::[] ;
val example_claim =
(Claim_judgment_proof ((Judgment_follows (example_premises) ((Prop_and ((Prop_p (#"p"::[] ))) ((Prop_p (#"q"::[] ))))))) (example_proof));
if valid_claim_dec_cake example_claim then print "True\n" else print "False\n";
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment