aboutsummaryrefslogtreecommitdiff
path: root/hott/Identity.thy (unfollow)
Commit message (Collapse)AuthorFilesLines
2020-08-14(FEAT) Context data slots for known types and conditional type rules, as ↵Josh Chen1-22/+25
well as a separate one for judgmental equality rules. (REF) Goal statement assumptions are now put into the new context data slots. (FEAT) `assuming` Isar keyword—like `assume` but puts assumptions into context data. (REF) Typechecking and all other tactics refactored to use type information from the context data, as opposed to looking at all facts visible in context. MINOR INCOMPATIBILITY: facts that were implicitly used in proofs now have to be annotated with [type] to make them visible throughout the context, else explicitly passed to methods via `using`, or declared with `assuming`. (REF) Fixed incompatibilities in theories.
2020-08-051. fix intros method. 2. Couple extra lemmas; good small test cases for ↵Josh Chen1-0/+40
normalization in typechecking/elaboration.
2020-08-03(FEAT) SIDE_CONDS tactical has additional argument specifying how many ↵Josh Chen1-1/+1
initial subgoals to skip applying the side condition solver to. (FEAT) `intro`, `intros` methods for "logical introduction rules" (as opposed to typechecking `intr` attribute), only works on conclusions with rigid type. (FEAT) CREPEAT_N bounded repetition tactical, used in `intros n` method.
2020-07-31(REF) Tweak attribute names in preparation for new logical introduction rule ↵Josh Chen1-2/+2
behavior
2020-07-31(FEAT) Term elaboration of assumption and goal statements.Josh Chen1-120/+119
. spartan/core/goals.ML . spartan/core/elaboration.ML . spartan/core/elaborated_statement.ML (FEAT) More context tacticals and search tacticals. . spartan/core/context_tactical.ML (FEAT) Improved subgoal focus. Moves fully elaborated assumptions into the context (MINOR INCOMPATIBILITY). . spartan/core/focus.ML (FIX) Normalize facts in order to be able to resolve properly. . spartan/core/typechecking.ML (MAIN) New definitions. (MAIN) Renamed theories and theorems. (MAIN) Refactor theories to fit new features.
2020-07-27Hook elaboration into assumptions mechanismJosh Chen1-40/+42
2020-07-211. Bugfix: implicits now properly name schematic variables. Fixes problems ↵Josh Chen1-7/+10
caused by variable name clashes. 2. reduce method now more principled: restricts to repeating on first subgoal. 3. An example declarative proof in Equivalence.thy.
2020-07-211. Type-checking/inference now more principled, and the implementation is ↵Josh Chen1-78/+69
better. 2. Changed most tactics to context tactics.
2020-07-09Non-annotated object lambdaJosh Chen1-4/+4
2020-07-08minorJosh Chen1-2/+2
2020-06-01reorganize and add some materialJosh Chen1-3/+3
2020-05-31transport methodJosh Chen1-0/+2
2020-05-29clean up Eckmann-Hilton and move to IdentityJosh Chen1-0/+181
2020-05-27minorJosh Chen1-0/+1
2020-05-27Eckmann-Hilton, first passJosh Chen1-0/+16
2020-05-26new materialJosh Chen1-23/+5
2020-05-25Lists + more reorganizingJosh Chen1-2/+2
2020-05-25Reorganize theory structure. In particular, the identity type moves out from ↵Josh Chen1-0/+0
under Spartan to HoTT. Spartan now only has Pi and Sigma.
2020-05-25slightly nicer homotopy proofs with calculationsJosh Chen1-1/+2
2020-05-25use existing calculation infrastructure for sym and transJosh Chen1-12/+3
2020-05-251. equality method now uses general elimination tactic. 2. New constant `` ↵Josh Chen1-51/+89
refers to rhs of equalities.
2020-05-24new work on elimination tacticJosh Chen1-1/+1
2020-05-22some tweaks and comments, in preparation for general inductive type eliminationJosh Chen1-6/+7
2020-04-021. make id function an abbrev. 2. fix reduce methodJosh Chen1-1/+1
2020-04-02Brand-spanking new version using Spartan infrastructureJosh Chen1-0/+433