Rocoma.Main

Summary: assumptions and proofs

This file was partially generated by Claude (Anthropic).

The rules on valid, stated as a module type. The development is parametrised by a module V : VALID.

Print VALID.

They are satisfied: Model : VALID in Recipes_valid_model interprets formulas in Prop.

Syntax: types (signatures), recipes, formulas.

Print type.
Print recipe.
Print term.
Print order.

Typing, with a forbidden window a,b) of free term variables.

Print has_type.
Print complete.

Stacks and application chains s ∘ l.

Print stack_item.
Print appl.

Evaluation ⟦ s ∘ l ⟧ of a complete recipe into a formula.

Print eval.
Print tractable.

Neutralisation.

Print neu.
Print neutral.

Logical relations.

Print logrel.
Print logrel2.
Print logrel3.
Print stack_rel.
Print aligned.
Print strongly.
Print strongly2.

Entailment, equivalence, meets.

Print entails.
Print ENT.
Print EQU.
Print fusion.
Print meet.
Print MEET.

Jokers (Fig. 6) and submission (appendix D).

Print joker_abs.
Print joker.
Print submits.
Print SUB.

Check logical_relation_lemma. (* Lemma 3.1 *)
Check logical_relation_lemma2.
Check eval_def. (* Theorem 3.2 *)
Check exists_unique_eval.
Check neuneug. (* Lemma 3.3 *)
Check entails_refl. (* Lemma 3.4 *)
Check entails_trans. (* Lemma 3.5 *)
Check entails_36. (* Lemma 3.6 *)
Check fusion_meet. (* Lemma 3.7 *)
Check cross_lemma. (* Corollary 3.8 *)
Check entails_neu. (* Corollary 3.9 *)
Check l_3_10. (* Lemma 3.10 *)
Check c_3_10_3.
Check c_3_10_4.
Check d1. (* Lemma D.1 *)
Check joker_entails. (* Theorem 3.11 *)

Functional evaluator, extracted to OCaml in Extraction.

All the results above together: besides the parameters of V, only functional extensionality.

The model of VALID only uses functional extensionality.