"""The full held-out test: all twenty steps of dalil al-kalima (7) and dalil al-imkan (13).

STATEMENTS ONLY -- never any proof. The model sees a goal exactly as Rocq displays it.
Eight of the twenty were in the first test (pilot.TASKS); the other twelve are added
here, transcribed from the theorem statements on the two results pages, in the
vocabulary of the pilot preamble (Ess = EssenceIncludesExistence).

    dalil al-kalima                              task id
    1  the four possibilities are the only ones  pr001_relational_exhaustive   (first test)
    2  self-creation is impossible               pr002_no_self_creation        (first test)
    3  circular creation is impossible           pr003_no_circle               (first test)
    4  no infinite regress of giving (key step)  pr004_no_two_step_giving      (first test)
    C  the conclusion, given the premises        kalima_first_cause            (first test)
    U  the universe is caused                    pr011_something_caused        (first test)
    C+U the conclusion without the "if"          kalima_unconditional
    dalil al-imkan
    1  the division                              imkan_s1_division
    2  the necessary cannot fail                 imkan_s2_necessary_cannot_fail
    3  the possible needs a cause                step3_possible_needs_cause    (first test)
    4  nothing causes itself                     imkan_s4_no_self_causation
    5  no possible lies outside the aggregate    imkan_s5_none_outside
    6  the aggregate is possible, needs a cause  imkan_s6_aggregate_possible_caused
    7  its cause is not a member                 imkan_s7_cause_not_member
    8  nothing made only of possibles causes it  imkan_s8_no_internal_cause
    9  its cause lies outside, and is not possible  imkan_s9_cause_outside
    10 an existing cause outside is necessary    imkan_s10_cause_necessary
    11 the aggregate has a necessary cause       imkan_s11_necessary_cause
    12 a Necessary Existent exists               imkan_s12_necessary_exists
    b  the short route                           imkan_b_necessary_exists      (first test)
"""
import sys
from pathlib import Path
sys.path.insert(0, str(Path(__file__).resolve().parent.parent / "pilot"))
import pilot

EXTRA = r"""
(* Added for the full test: aggregates, possible worlds, and their postulates. *)
Variable MemberOf : Thing -> Thing -> Prop.  (* p is a member of the aggregate a *)
Variable World : Type.
Variable ExistsIn : World -> Thing -> Prop.  (* x exists in world w *)
Definition Independent (x : Thing) : Prop := forall y, ~ DependsOn x y.
Definition NonExistencePossible (x : Thing) : Prop := exists w, ~ ExistsIn w x.
Definition AggregateOfPossibles (A : Thing) : Prop :=
  (forall p, p <> A -> (MemberOf p A <-> Possible p)) /\ ~ MemberOf A A.
Definition MP007 : Prop := forall x, Ess x -> forall w, ExistsIn w x.        (* existence from one's nature cannot fail *)
Definition MP009 : Prop := (exists p, Possible p) -> exists A, AggregateOfPossibles A /\ Exists A.  (* the aggregate of possibles exists *)
Definition MP010 : Prop := forall A, (exists p, MemberOf p A) ->
  (forall p, MemberOf p A -> ~ Ess p) -> ~ Ess A.                            (* possibles do not add up to a necessary *)
Definition MP011 : Prop := forall c A p, Gives c A -> MemberOf p A -> clos_trans Thing Gives c p.  (* giving to a whole gives to its members *)
Definition MP012 : Prop := forall y x, Gives y x -> Exists y.               (* a giver exists *)
"""
PREAMBLE = pilot.PREAMBLE + EXTRA

NEW = {
 "kalima_unconditional":
   "MP001 -> MP002 -> MP003 -> OP001 -> MP008 -> OP006 -> "
   "exists x b, InUniverse x /\\ Gives b x /\\ Exists b /\\ Necessary b /\\ Independent b",
 "imkan_s1_division":
   "forall x, Exists x -> (Necessary x \\/ Possible x) /\\ ~ (Necessary x /\\ Possible x)",
 "imkan_s2_necessary_cannot_fail":
   "MP007 -> forall x, Necessary x -> ~ NonExistencePossible x",
 "imkan_s4_no_self_causation":
   "MP001 -> MP002 -> forall A, ~ Gives A A",
 "imkan_s5_none_outside":
   "forall A, AggregateOfPossibles A -> forall p, p <> A -> Possible p -> MemberOf p A",
 "imkan_s6_aggregate_possible_caused":
   "MP008 -> MP010 -> forall A, AggregateOfPossibles A -> Exists A -> "
   "(exists p, p <> A /\\ Possible p) -> Possible A /\\ ThroughAnother A",
 "imkan_s7_cause_not_member":
   "MP001 -> MP002 -> MP003 -> MP011 -> forall c A, Gives c A -> ~ MemberOf c A",
 "imkan_s8_no_internal_cause":
   "MP001 -> MP002 -> MP003 -> MP010 -> MP011 -> forall A, AggregateOfPossibles A -> "
   "(forall x, ~ Gives x x) /\\ ~ Gives A A /\\ (forall c, MemberOf c A -> ~ Gives c A) /\\ "
   "(forall B, B <> A -> Exists B -> (exists p, MemberOf p B) -> (forall p, MemberOf p B -> MemberOf p A) -> ~ Gives B A)",
 "imkan_s9_cause_outside":
   "MP001 -> MP002 -> MP003 -> MP011 -> forall A c, AggregateOfPossibles A -> Gives c A -> "
   "~ MemberOf c A /\\ c <> A /\\ ~ Possible c",
 "imkan_s10_cause_necessary":
   "MP001 -> MP002 -> MP003 -> MP011 -> MP012 -> forall A c, AggregateOfPossibles A -> Gives c A -> Necessary c",
 "imkan_s11_necessary_cause":
   "MP001 -> MP002 -> MP003 -> MP008 -> MP010 -> MP011 -> MP012 -> forall A, AggregateOfPossibles A -> Exists A -> "
   "(exists p, p <> A /\\ Possible p) -> exists c, Gives c A /\\ Necessary c /\\ ~ MemberOf c A /\\ c <> A",
 "imkan_s12_necessary_exists":
   "MP001 -> MP002 -> MP003 -> MP008 -> MP009 -> MP010 -> MP011 -> MP012 -> SP001 -> exists n, Necessary n",
}
TASKS = {**pilot.TASKS, **NEW}
assert len(TASKS) == 20