Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Definition of weak-head-reduction and proof of unicity of derivations #543

Draft
wants to merge 208 commits into
base: coq-8.11
Choose a base branch
from
Draft

Definition of weak-head-reduction and proof of unicity of derivations #543

wants to merge 208 commits into from

Commits on Dec 13, 2020

  1. WIP

    @jakobbotsch @mattam82
    jakobbotsch authored and mattam82 committed Dec 13, 2020
    Configuration menu
    Copy the full SHA
    8434f9f View commit details
    Browse the repository at this point in the history

  2. WIP

    @jakobbotsch @mattam82
    jakobbotsch authored and mattam82 committed Dec 13, 2020
    Configuration menu
    Copy the full SHA
    316f303 View commit details
    Browse the repository at this point in the history

Commits on Dec 14, 2020

  1. Updated template-coq to new case representation

    @mattam82
    mattam82 committed Dec 14, 2020
    Configuration menu
    Copy the full SHA
    94fe9bf View commit details
    Browse the repository at this point in the history

  2. Started updating PCUIC

    @mattam82
    mattam82 committed Dec 14, 2020
    Configuration menu
    Copy the full SHA
    0abf8ec View commit details
    Browse the repository at this point in the history

  3. WIP in lift_subst. Needs better solve_all

    @mattam82
    mattam82 committed Dec 14, 2020
    Configuration menu
    Copy the full SHA
    9c742bb View commit details
    Browse the repository at this point in the history

Commits on Dec 15, 2020

  1. Extend All_Forall with OnOne2i theory

    @mattam82
    mattam82 committed Dec 15, 2020
    Configuration menu
    Copy the full SHA
    1657d71 View commit details
    Browse the repository at this point in the history

  2. Update typing and reduction to new branch representation. Also factor… 

    …ize / cleanup a bit more.
    @mattam82
    mattam82 committed Dec 15, 2020
    Configuration menu
    Copy the full SHA
    67e2469 View commit details
    Browse the repository at this point in the history

Commits on Dec 16, 2020

  1. Generalize map_predicate to take a universe instance mapping function.

    @mattam82
    mattam82 committed Dec 16, 2020
    Configuration menu
    Copy the full SHA
    ef2f53c View commit details
    Browse the repository at this point in the history

  2. WP in PCUIC

    @mattam82
    mattam82 committed Dec 16, 2020
    Configuration menu
    Copy the full SHA
    1b73236 View commit details
    Browse the repository at this point in the history

Commits on Dec 17, 2020

  1. WIP in reduction

    @mattam82
    mattam82 committed Dec 17, 2020
    Configuration menu
    Copy the full SHA
    84c53b3 View commit details
    Browse the repository at this point in the history

Commits on Dec 19, 2020

  1. New PCUICCases file with context building predicates. Finished updati… 

    …ng PCUICTyping
    @mattam82
    mattam82 committed Dec 19, 2020
    Configuration menu
    Copy the full SHA
    f502f79 View commit details
    Browse the repository at this point in the history

  2. Improve predicate equality to take care of binder relevance annotations

    @mattam82
    mattam82 committed Dec 19, 2020
    Configuration menu
    Copy the full SHA
    533bef5 View commit details
    Browse the repository at this point in the history

  3. Finished (partial) PCUICNameless proof

    @mattam82
    mattam82 committed Dec 19, 2020
    Configuration menu
    Copy the full SHA
    bae4d15 View commit details
    Browse the repository at this point in the history

  4. WIP in PCUICClosed

    @mattam82
    mattam82 committed Dec 19, 2020
    Configuration menu
    Copy the full SHA
    a9c5ab8 View commit details
    Browse the repository at this point in the history

  5. Finished PCUICClosed

    @mattam82
    mattam82 committed Dec 19, 2020
    Configuration menu
    Copy the full SHA
    50f153d View commit details
    Browse the repository at this point in the history

  6. In PCUICNormal. will need to rely on wf environment

    @mattam82
    mattam82 committed Dec 19, 2020
    Configuration menu
    Copy the full SHA
    49909c5 View commit details
    Browse the repository at this point in the history

Commits on Dec 21, 2020

  1. Trying to find the right hypotheses on reduction: everything gets ugl… 

    …y if we don't have direct access to the indices of the inductive and the arguments of constructors (due to "instantiate_params" and destArity getting in the way).
    @mattam82
    mattam82 committed Dec 21, 2020
    Configuration menu
    Copy the full SHA
    b1f09a6 View commit details
    Browse the repository at this point in the history

  2. Bite the bullet and cleanup the representation of constructors of ind… 

    …uctives in the environment. Direct access to the contexts of indices and sort of an indutive, and constructor arguments and conclusion indices.
    @mattam82
    mattam82 committed Dec 21, 2020
    Configuration menu
    Copy the full SHA
    30c94e2 View commit details
    Browse the repository at this point in the history

  3. WIP with cleaned-up inductive and constructor representation

    @mattam82
    mattam82 committed Dec 21, 2020
    Configuration menu
    Copy the full SHA
    a3d5866 View commit details
    Browse the repository at this point in the history

  4. WIP renaming

    @mattam82
    mattam82 committed Dec 21, 2020
    Configuration menu
    Copy the full SHA
    0f21b68 View commit details
    Browse the repository at this point in the history

  5. Done up to TypingWf

    @mattam82
    mattam82 committed Dec 21, 2020
    Configuration menu
    Copy the full SHA
    7a73d53 View commit details
    Browse the repository at this point in the history

  6. Updated upto PCUICTyping

    @mattam82
    mattam82 committed Dec 21, 2020
    Configuration menu
    Copy the full SHA
    e4aae53 View commit details
    Browse the repository at this point in the history

  7. PCUICNormal working now

    @mattam82
    mattam82 committed Dec 21, 2020
    Configuration menu
    Copy the full SHA
    54ed6d4 View commit details
    Browse the repository at this point in the history

  8. Directly map on constructor list in case reduction

    @mattam82
    mattam82 committed Dec 21, 2020
    Configuration menu
    Copy the full SHA
    ebc9216 View commit details
    Browse the repository at this point in the history

  9. Now in sigmacalculus. Need to cleanup substitution/lifting lemmas for… 

    … lets first.
    @mattam82
    mattam82 committed Dec 21, 2020
    Configuration menu
    Copy the full SHA
    138ca1f View commit details
    Browse the repository at this point in the history

Commits on Dec 22, 2020

  1. WIP proviing renaming lemma

    @mattam82
    mattam82 committed Dec 22, 2020
    Configuration menu
    Copy the full SHA
    a9f14aa View commit details
    Browse the repository at this point in the history

  2. Cleanup PCUICClosed to use the right unfolding behaviors

    @mattam82
    mattam82 committed Dec 22, 2020
    Configuration menu
    Copy the full SHA
    676f1b2 View commit details
    Browse the repository at this point in the history

Commits on Dec 23, 2020

  1. Almost complete nameless proof

    @mattam82
    mattam82 committed Dec 23, 2020
    Configuration menu
    Copy the full SHA
    c61c55c View commit details
    Browse the repository at this point in the history

  2. De bruijn bug in map_constructor_body...

    @mattam82
    mattam82 committed Dec 23, 2020
    Configuration menu
    Copy the full SHA
    be5f608 View commit details
    Browse the repository at this point in the history

  3. Cleaning up sigma calculus proofs

    @mattam82
    mattam82 committed Dec 23, 2020
    Configuration menu
    Copy the full SHA
    528de5b View commit details
    Browse the repository at this point in the history

  4. Fix replace.sh

    @mattam82
    mattam82 committed Dec 23, 2020
    Configuration menu
    Copy the full SHA
    6714426 View commit details
    Browse the repository at this point in the history

  5. Switched arguments of declared_inductive

    @mattam82
    mattam82 committed Dec 23, 2020
    Configuration menu
    Copy the full SHA
    4f55189 View commit details
    Browse the repository at this point in the history

  6. Fic declared_constructor argument order

    @mattam82
    mattam82 committed Dec 23, 2020
    Configuration menu
    Copy the full SHA
    ff845cc View commit details
    Browse the repository at this point in the history

  7. Change declared_projection argument order

    @mattam82
    mattam82 committed Dec 23, 2020
    Configuration menu
    Copy the full SHA
    c294bd7 View commit details
    Browse the repository at this point in the history

  8. Big refactoring / cleanup of sigma calculus

    @mattam82
    mattam82 committed Dec 23, 2020
    Configuration menu
    Copy the full SHA
    bd32ff3 View commit details
    Browse the repository at this point in the history

  9. SigmaCalculus is now self-contained and does not depend on Closed

    @mattam82
    mattam82 committed Dec 23, 2020
    Configuration menu
    Copy the full SHA
    289b8b5 View commit details
    Browse the repository at this point in the history

Commits on Dec 24, 2020

  1. Better induction principle for "generated" contexts (fix/case/branches)

    @mattam82
    mattam82 committed Dec 24, 2020
    Configuration menu
    Copy the full SHA
    0a205ee View commit details
    Browse the repository at this point in the history

  2. Refactoring and proving renaming theorem

    @mattam82
    mattam82 committed Dec 24, 2020
    Configuration menu
    Copy the full SHA
    fbd5584 View commit details
    Browse the repository at this point in the history

  3. Completed renaming proof with new case.

    @mattam82
    mattam82 committed Dec 24, 2020
    Configuration menu
    Copy the full SHA
    d18eb24 View commit details
    Browse the repository at this point in the history

  4. Prove weakening... from instantiation

    @mattam82
    mattam82 committed Dec 24, 2020
    Configuration menu
    Copy the full SHA
    dc507c2 View commit details
    Browse the repository at this point in the history

Commits on Dec 26, 2020

  1. Strenghten renaming theorem for exchange and strengthening.

    @mattam82
    mattam82 committed Dec 26, 2020
    Configuration menu
    Copy the full SHA
    f7a3612 View commit details
    Browse the repository at this point in the history

  2. WIP finishing strengthening

    @mattam82
    mattam82 committed Dec 26, 2020
    Configuration menu
    Copy the full SHA
    bc2366b View commit details
    Browse the repository at this point in the history

  3. WIP on renaming proofs carrying variable information

    @mattam82
    mattam82 committed Dec 26, 2020
    Configuration menu
    Copy the full SHA
    8a5c296 View commit details
    Browse the repository at this point in the history

Commits on Dec 27, 2020

  1. Finished proof that reduction preserves free variables

    @mattam82
    mattam82 committed Dec 27, 2020
    Configuration menu
    Copy the full SHA
    2f37033 View commit details
    Browse the repository at this point in the history

  2. Need to think about how to state the exchange lemma

    @mattam82
    mattam82 committed Dec 27, 2020
    Configuration menu
    Copy the full SHA
    78881fd View commit details
    Browse the repository at this point in the history

  3. Proven renaming for shiftnP predicate

    @mattam82
    mattam82 committed Dec 27, 2020
    Configuration menu
    Copy the full SHA
    537b9d3 View commit details
    Browse the repository at this point in the history

Commits on Dec 28, 2020

  1. Play with strengthening: not provable inductively as conversions can … 

    …include arbitrary terms
    @mattam82
    mattam82 committed Dec 28, 2020
    Configuration menu
    Copy the full SHA
    d2df801 View commit details
    Browse the repository at this point in the history

  2. Verified proof idea for strengthening (will have to come after subjec… 

    …t reduction)
    @mattam82
    mattam82 committed Dec 28, 2020
    Configuration menu
    Copy the full SHA
    5dd9644 View commit details
    Browse the repository at this point in the history

Commits on Jan 4, 2021

  1. Cleanup Weakening, move on_free_vars to a separate library

    @mattam82
    mattam82 committed Jan 4, 2021
    Configuration menu
    Copy the full SHA
    2a53557 View commit details
    Browse the repository at this point in the history

  2. WIP in instantiation theorem

    @mattam82
    mattam82 committed Jan 4, 2021
    Configuration menu
    Copy the full SHA
    82c7d4e View commit details
    Browse the repository at this point in the history

Commits on Jan 5, 2021

  1. Only instantiation for cumulativity remaining

    @mattam82
    mattam82 committed Jan 5, 2021
    Configuration menu
    Copy the full SHA
    eb7f0b4 View commit details
    Browse the repository at this point in the history

  2. Only eq_term upto instantiation remains

    @mattam82
    mattam82 committed Jan 5, 2021
    Configuration menu
    Copy the full SHA
    80c662c View commit details
    Browse the repository at this point in the history

  3. Finished instantiation proof

    @mattam82
    mattam82 committed Jan 5, 2021
    Configuration menu
    Copy the full SHA
    1e119c6 View commit details
    Browse the repository at this point in the history

Commits on Jan 6, 2021

  1. Updating substitution and universe instantiation

    @mattam82
    mattam82 committed Jan 6, 2021
    Configuration menu
    Copy the full SHA
    81aa326 View commit details
    Browse the repository at this point in the history

  2. Before moving to overloaded subst_instance operation everywhere

    @mattam82
    mattam82 committed Jan 6, 2021
    Configuration menu
    Copy the full SHA
    6f8fdd9 View commit details
    Browse the repository at this point in the history

  3. Use overloaded subst_instance in template-coq

    @mattam82
    mattam82 committed Jan 6, 2021
    Configuration menu
    Copy the full SHA
    24e6b2c View commit details
    Browse the repository at this point in the history

  4. Cleanup name of subst_instance lemmatas

    @mattam82
    mattam82 committed Jan 6, 2021
    Configuration menu
    Copy the full SHA
    43c13cc View commit details
    Browse the repository at this point in the history

  5. Half of universe instantiation done

    @mattam82
    mattam82 committed Jan 6, 2021
    Configuration menu
    Copy the full SHA
    3da3351 View commit details
    Browse the repository at this point in the history

Commits on Jan 7, 2021

  1. Updated univ substitution

    @mattam82
    mattam82 committed Jan 7, 2021
    Configuration menu
    Copy the full SHA
    9e58182 View commit details
    Browse the repository at this point in the history

  2. Finished implementing substitution through instantiation. substitutio… 

    …n lemma remains
    @mattam82
    mattam82 committed Jan 7, 2021
    Configuration menu
    Copy the full SHA
    50190ca View commit details
    Browse the repository at this point in the history

  3. WIP in substitution lemmas

    @mattam82
    mattam82 committed Jan 7, 2021
    Configuration menu
    Copy the full SHA
    3f6d0b8 View commit details
    Browse the repository at this point in the history

Commits on Jan 8, 2021

  1. Finished substitution

    @mattam82
    mattam82 committed Jan 8, 2021
    Configuration menu
    Copy the full SHA
    c2be5a1 View commit details
    Browse the repository at this point in the history

  2. Updating Parallel Reduction to carry well-formedness predicates

    @mattam82
    mattam82 committed Jan 8, 2021
    Configuration menu
    Copy the full SHA
    bb61a04 View commit details
    Browse the repository at this point in the history

  3. Try a simpler solution for pred allowing reflexivity on case

    @mattam82
    mattam82 committed Jan 8, 2021
    Configuration menu
    Copy the full SHA
    fe9dfa2 View commit details
    Browse the repository at this point in the history

  4. WIP

    @mattam82
    mattam82 committed Jan 8, 2021
    Configuration menu
    Copy the full SHA
    ec88526 View commit details
    Browse the repository at this point in the history

Commits on Jan 11, 2021

  1. Move to PCUIC having expanded contexts in Case nodes

    @mattam82
    mattam82 committed Jan 11, 2021
    Configuration menu
    Copy the full SHA
    a891b73 View commit details
    Browse the repository at this point in the history

  2. Template <-> PCUIC translations defined

    @mattam82
    mattam82 committed Jan 11, 2021
    Configuration menu
    Copy the full SHA
    f954b2c View commit details
    Browse the repository at this point in the history

  3. Main infrastructure lemmas on contexts in cases proven

    @mattam82
    mattam82 committed Jan 11, 2021
    Configuration menu
    Copy the full SHA
    dc07622 View commit details
    Browse the repository at this point in the history

Commits on Jan 12, 2021

  1. Updated SigmaCalculus proofs

    @mattam82
    mattam82 committed Jan 12, 2021
    Configuration menu
    Copy the full SHA
    2fe7460 View commit details
    Browse the repository at this point in the history

  2. WIP in equality, now needing context equality

    @mattam82
    mattam82 committed Jan 12, 2021
    Configuration menu
    Copy the full SHA
    5cca998 View commit details
    Browse the repository at this point in the history

  3. Updated Equality

    @mattam82
    mattam82 committed Jan 12, 2021
    Configuration menu
    Copy the full SHA
    13d4718 View commit details
    Browse the repository at this point in the history

  4. WIP in simplifying reduction

    @mattam82
    mattam82 committed Jan 12, 2021
    Configuration menu
    Copy the full SHA
    cafa9de View commit details
    Browse the repository at this point in the history

Commits on Jan 13, 2021

  1. Updated Typing to add new context conversion premisses

    @mattam82
    mattam82 committed Jan 13, 2021
    Configuration menu
    Copy the full SHA
    dd0481f View commit details
    Browse the repository at this point in the history

  2. WeakeningEnv and Nameless updated

    @mattam82
    mattam82 committed Jan 13, 2021
    Configuration menu
    Copy the full SHA
    7db4e9b View commit details
    Browse the repository at this point in the history

  3. Move EqDec instance for Ast.term away from Reflect, so as not to poll… 

    …ute PCUIC
    @mattam82
    mattam82 committed Jan 13, 2021
    Configuration menu
    Copy the full SHA
    c2be4d0 View commit details
    Browse the repository at this point in the history

  4. Fix module includes to avoid growing rewrite databases for nothing

    @mattam82
    mattam82 committed Jan 13, 2021
    Configuration menu
    Copy the full SHA
    e803b97 View commit details
    Browse the repository at this point in the history

  5. Adapted PCUICNormal

    @mattam82
    mattam82 committed Jan 13, 2021
    Configuration menu
    Copy the full SHA
    e358ebe View commit details
    Browse the repository at this point in the history

Commits on Jan 14, 2021

  1. WIP in PCUICClosed

    @mattam82
    mattam82 committed Jan 14, 2021
    Configuration menu
    Copy the full SHA
    51005a2 View commit details
    Browse the repository at this point in the history

  2. Updated Closed

    @mattam82
    mattam82 committed Jan 14, 2021
    Configuration menu
    Copy the full SHA
    0df06e7 View commit details
    Browse the repository at this point in the history

  3. Fully adapted PCUICNameless

    @mattam82
    mattam82 committed Jan 14, 2021
    Configuration menu
    Copy the full SHA
    5d44820 View commit details
    Browse the repository at this point in the history

  4. Adapted OnFreeVars

    @mattam82
    mattam82 committed Jan 14, 2021
    Configuration menu
    Copy the full SHA
    1173229 View commit details
    Browse the repository at this point in the history

  5. Adapt PCUICUnivSubstitution

    @mattam82
    mattam82 committed Jan 14, 2021
    Configuration menu
    Copy the full SHA
    dd68d3c View commit details
    Browse the repository at this point in the history

Commits on Jan 15, 2021

  1. Adapted PCUICRename

    @mattam82
    mattam82 committed Jan 15, 2021
    Configuration menu
    Copy the full SHA
    1a304a5 View commit details
    Browse the repository at this point in the history

  2. Updated instantiation and substitution

    @mattam82
    mattam82 committed Jan 15, 2021
    Configuration menu
    Copy the full SHA
    02827eb View commit details
    Browse the repository at this point in the history

  3. Need a new reduction rule on contexts as expected

    @mattam82
    mattam82 committed Jan 15, 2021
    Configuration menu
    Copy the full SHA
    8dbf957 View commit details
    Browse the repository at this point in the history

Commits on Jan 16, 2021

  1. WIP adapting Reduction to new reduction rules on contexts in cases

    @mattam82
    mattam82 committed Jan 16, 2021
    Configuration menu
    Copy the full SHA
    94bab92 View commit details
    Browse the repository at this point in the history

  2. Updating UnivSubstitution

    @mattam82
    mattam82 committed Jan 16, 2021
    Configuration menu
    Copy the full SHA
    8d10ecc View commit details
    Browse the repository at this point in the history

  3. WIP in reduction is good

    @mattam82
    mattam82 committed Jan 16, 2021
    Configuration menu
    Copy the full SHA
    3474c64 View commit details
    Browse the repository at this point in the history

Commits on Jan 17, 2021

  1. Complete the theory of context reduction 

    closure of red1 on one decl <-> context relation of reducing any term in the context
    @mattam82
    mattam82 committed Jan 17, 2021
    Configuration menu
    Copy the full SHA
    a4f294a View commit details
    Browse the repository at this point in the history

  2. Updated upto instantiation and normal

    @mattam82
    mattam82 committed Jan 17, 2021
    Configuration menu
    Copy the full SHA
    af59042 View commit details
    Browse the repository at this point in the history

  3. WIP lifting parallel reduction to new case context reductions

    @mattam82
    mattam82 committed Jan 17, 2021
    Configuration menu
    Copy the full SHA
    1b8909d View commit details
    Browse the repository at this point in the history

  4. Substitutivity of parallel reduction

    @mattam82
    mattam82 committed Jan 17, 2021
    Configuration menu
    Copy the full SHA
    beae36c View commit details
    Browse the repository at this point in the history

  5. WIP adapting rho function

    @mattam82
    mattam82 committed Jan 17, 2021
    Configuration menu
    Copy the full SHA
    f9135de View commit details
    Browse the repository at this point in the history

Commits on Jan 18, 2021

  1. WIP in confluence proof

    @mattam82
    mattam82 committed Jan 18, 2021
    Configuration menu
    Copy the full SHA
    c6b25ea View commit details
    Browse the repository at this point in the history

Commits on Jan 19, 2021

  1. Showing that rho_ctx is stable under renaming

    @mattam82
    mattam82 committed Jan 19, 2021
    Configuration menu
    Copy the full SHA
    289abdb View commit details
    Browse the repository at this point in the history

  2. WIP in parallel reduction confluence

    @mattam82
    mattam82 committed Jan 19, 2021
    Configuration menu
    Copy the full SHA
    fd4193a View commit details
    Browse the repository at this point in the history

Commits on Jan 20, 2021

  1. rho match case finished

    @mattam82
    mattam82 committed Jan 20, 2021
    Configuration menu
    Copy the full SHA
    12a894a View commit details
    Browse the repository at this point in the history

  2. Finished updating confluence proof

    @mattam82
    mattam82 committed Jan 20, 2021
    Configuration menu
    Copy the full SHA
    87c754e View commit details
    Browse the repository at this point in the history

  3. WIP in finishing confluence proof

    @mattam82
    mattam82 committed Jan 20, 2021
    Configuration menu
    Copy the full SHA
    1771da3 View commit details
    Browse the repository at this point in the history

  4. Move eq_predicate Equivalence instances in separate lemmas

    @mattam82
    mattam82 committed Jan 20, 2021
    Configuration menu
    Copy the full SHA
    f13b508 View commit details
    Browse the repository at this point in the history

  5. Shown commnutation of eq_term and reduction

    @mattam82
    mattam82 committed Jan 20, 2021
    Configuration menu
    Copy the full SHA
    967bd80 View commit details
    Browse the repository at this point in the history

  6. Need to fix problem of name preservation missing from All2_local_env

    @mattam82
    mattam82 committed Jan 20, 2021
    Configuration menu
    Copy the full SHA
    dfc0c54 View commit details
    Browse the repository at this point in the history

  7. Before replacing All2_local_env

    @mattam82
    mattam82 committed Jan 20, 2021
    Configuration menu
    Copy the full SHA
    8c05bb7 View commit details
    Browse the repository at this point in the history

Commits on Jan 21, 2021

  1. Factorize similar context relations into a general one

    @mattam82
    mattam82 committed Jan 21, 2021
    Configuration menu
    Copy the full SHA
    1e33a4f View commit details
    Browse the repository at this point in the history

  2. Adapted confluence proof to new, correct context relation structure

    @mattam82
    mattam82 committed Jan 21, 2021
    Configuration menu
    Copy the full SHA
    1484164 View commit details
    Browse the repository at this point in the history

  3. Back in confluence with the right definitions

    @mattam82
    mattam82 committed Jan 21, 2021
    Configuration menu
    Copy the full SHA
    b16284a View commit details
    Browse the repository at this point in the history

  4. Refine RedTypeIrrelevance: only body reduction matters

    @mattam82
    mattam82 committed Jan 21, 2021
    Configuration menu
    Copy the full SHA
    b60ac24 View commit details
    Browse the repository at this point in the history

  5. Finish confluence proofs (up to alpha-equivalence as well)

    @mattam82
    mattam82 committed Jan 21, 2021
    Configuration menu
    Copy the full SHA
    1ba2a31 View commit details
    Browse the repository at this point in the history

  6. Refine red type irrelevance: it preserves the step number

    @mattam82
    mattam82 committed Jan 21, 2021
    Configuration menu
    Copy the full SHA
    3be9be0 View commit details
    Browse the repository at this point in the history

  7. WIP in Context Conversion

    @mattam82
    mattam82 committed Jan 21, 2021
    Configuration menu
    Copy the full SHA
    6426108 View commit details
    Browse the repository at this point in the history

  8. Context Cumulativity/Conversion done

    @mattam82
    mattam82 committed Jan 21, 2021
    Configuration menu
    Copy the full SHA
    692473a View commit details
    Browse the repository at this point in the history

  9. Now in the safe zone :) Adapting conversion lemmas

    @mattam82
    mattam82 committed Jan 21, 2021
    Configuration menu
    Copy the full SHA
    e67b09a View commit details
    Browse the repository at this point in the history

Commits on Jan 22, 2021

  1. Fix definition of comparison of declarations

    @mattam82
    mattam82 committed Jan 22, 2021
    Configuration menu
    Copy the full SHA
    8ee93d4 View commit details
    Browse the repository at this point in the history

  2. Finished conversion (one todo left)

    @mattam82
    mattam82 committed Jan 22, 2021
    Configuration menu
    Copy the full SHA
    60a73ed View commit details
    Browse the repository at this point in the history

  3. In inversion

    @mattam82
    mattam82 committed Jan 22, 2021
    Configuration menu
    Copy the full SHA
    2f6fb43 View commit details
    Browse the repository at this point in the history

  4. TODOs in PCUICToTemplate

    @mattam82
    mattam82 committed Jan 22, 2021
    Configuration menu
    Copy the full SHA
    4bc6923 View commit details
    Browse the repository at this point in the history

  5. Remove unused PCUICtxShape

    @mattam82
    mattam82 committed Jan 22, 2021
    Configuration menu
    Copy the full SHA
    f8d1a0c View commit details
    Browse the repository at this point in the history

  6. Before renaming fold_context

    @mattam82
    mattam82 committed Jan 22, 2021
    Configuration menu
    Copy the full SHA
    2f220ef View commit details
    Browse the repository at this point in the history

  7. WIP renaming fold_context to fold_context_k

    @mattam82
    mattam82 committed Jan 22, 2021
    Configuration menu
    Copy the full SHA
    61b6bb8 View commit details
    Browse the repository at this point in the history

  8. TODOs

    @mattam82
    mattam82 committed Jan 22, 2021
    Configuration menu
    Copy the full SHA
    45706c5 View commit details
    Browse the repository at this point in the history

  9. Adapted Inductives (rather easily!)

    @mattam82
    mattam82 committed Jan 22, 2021
    Configuration menu
    Copy the full SHA
    c805902 View commit details
    Browse the repository at this point in the history

Commits on Jan 23, 2021

  1. WIP in InductiveInversion

    @mattam82
    mattam82 committed Jan 23, 2021
    Configuration menu
    Copy the full SHA
    3dae729 View commit details
    Browse the repository at this point in the history

  2. Finished updating InductiveInversion!

    @mattam82
    mattam82 committed Jan 23, 2021
    Configuration menu
    Copy the full SHA
    801b5ad View commit details
    Browse the repository at this point in the history

  3. Adapted SR (todos for Case)

    @mattam82
    mattam82 committed Jan 23, 2021
    Configuration menu
    Copy the full SHA
    b1c14d4 View commit details
    Browse the repository at this point in the history

  4. Adapted TemplateToPCUIC (most is todo, corrected statement of transla… 

    …tion theorem though)
    @mattam82
    mattam82 committed Jan 23, 2021
    Configuration menu
    Copy the full SHA
    710919d View commit details
    Browse the repository at this point in the history

  5. Updated Alpha conversion proof. Could be derivable from nameless (or … 

    …the other way around)
    @mattam82
    mattam82 committed Jan 23, 2021
    Configuration menu
    Copy the full SHA
    d328f95 View commit details
    Browse the repository at this point in the history

  6. Adapted WcbvEval entirely

    @mattam82
    mattam82 committed Jan 23, 2021
    Configuration menu
    Copy the full SHA
    f7b4c00 View commit details
    Browse the repository at this point in the history

  7. Adapted SafeLemmatas, some todos on stacks left

    @mattam82
    mattam82 committed Jan 23, 2021
    Configuration menu
    Copy the full SHA
    fad7667 View commit details
    Browse the repository at this point in the history

  8. SN and cumulprop done (some todos left)

    @mattam82
    mattam82 committed Jan 23, 2021
    Configuration menu
    Copy the full SHA
    5684127 View commit details
    Browse the repository at this point in the history

  9. Principality with todos (does not look too hard :)

    @mattam82
    mattam82 committed Jan 23, 2021
    Configuration menu
    Copy the full SHA
    888f66b View commit details
    Browse the repository at this point in the history

  10. Fixed elimination (little change in statements)

    @mattam82
    mattam82 committed Jan 23, 2021
    Configuration menu
    Copy the full SHA
    00147fa View commit details
    Browse the repository at this point in the history

  11. Canonicity and ConvCumInversion (with some admits)

    @mattam82
    mattam82 committed Jan 23, 2021
    Configuration menu
    Copy the full SHA
    ca6542e View commit details
    Browse the repository at this point in the history

Commits on Jan 24, 2021

  1. Updated WfReduction (no todos)

    @mattam82
    mattam82 committed Jan 24, 2021
    Configuration menu
    Copy the full SHA
    6c81863 View commit details
    Browse the repository at this point in the history

  2. PCUICErrors updated

    @mattam82
    mattam82 committed Jan 24, 2021
    Configuration menu
    Copy the full SHA
    b6bc547 View commit details
    Browse the repository at this point in the history

  3. Adapted EqualityDec

    @mattam82
    mattam82 committed Jan 24, 2021
    Configuration menu
    Copy the full SHA
    c60a54f View commit details
    Browse the repository at this point in the history

  4. Fix weird bug with make vos in WcbvEval

    @mattam82
    mattam82 committed Jan 24, 2021
    Configuration menu
    Copy the full SHA
    b5950b2 View commit details
    Browse the repository at this point in the history

  5. Updated EqualityDec

    @mattam82
    mattam82 committed Jan 24, 2021
    Configuration menu
    Copy the full SHA
    0d696d4 View commit details
    Browse the repository at this point in the history

  6. Safe Reduce updated (with todos)

    @mattam82
    mattam82 committed Jan 24, 2021
    Configuration menu
    Copy the full SHA
    1811999 View commit details
    Browse the repository at this point in the history

  7. Fix definitions of predicate/branch conversion

    @mattam82
    mattam82 committed Jan 24, 2021
    Configuration menu
    Copy the full SHA
    63cca49 View commit details
    Browse the repository at this point in the history

  8. In Safe Retyping

    @mattam82
    mattam82 committed Jan 24, 2021
    Configuration menu
    Copy the full SHA
    2a0b944 View commit details
    Browse the repository at this point in the history

  9. Updated SafeConversion

    @mattam82
    mattam82 committed Jan 24, 2021
    Configuration menu
    Copy the full SHA
    5d01f18 View commit details
    Browse the repository at this point in the history

Commits on Jan 25, 2021

  1. Finished updating safechecker (some todos left)

    @mattam82
    mattam82 committed Jan 25, 2021
    Configuration menu
    Copy the full SHA
    7821f3f View commit details
    Browse the repository at this point in the history

  2. Finished with the checker

    @mattam82
    mattam82 committed Jan 25, 2021
    Configuration menu
    Copy the full SHA
    3d8a8e8 View commit details
    Browse the repository at this point in the history

  3. Updated erasure (with some todos)

    @mattam82
    mattam82 committed Jan 25, 2021
    Configuration menu
    Copy the full SHA
    744d46d View commit details
    Browse the repository at this point in the history

Commits on Jan 26, 2021

  1. Update PCUICConversion, PCUICNormal, PCUICConvCumInversion

    @jakobbotsch
    jakobbotsch committed Jan 26, 2021
    Configuration menu
    Copy the full SHA
    8beb451 View commit details
    Browse the repository at this point in the history

Commits on Jan 27, 2021

  1. Update safe reduction soundness, still missing completeness

    @jakobbotsch
    jakobbotsch committed Jan 27, 2021
    Configuration menu
    Copy the full SHA
    d684cce View commit details
    Browse the repository at this point in the history

  2. Remove unneeded file

    @mattam82
    mattam82 committed Jan 27, 2021
    Configuration menu
    Copy the full SHA
    ad72f4a View commit details
    Browse the repository at this point in the history

  3. Update reification/quoting of inductives and cases

    @mattam82
    mattam82 committed Jan 27, 2021
    Configuration menu
    Copy the full SHA
    3d5c348 View commit details
    Browse the repository at this point in the history

  4. Remove spurious Locate command

    @mattam82
    mattam82 committed Jan 27, 2021
    Configuration menu
    Copy the full SHA
    675fbda View commit details
    Browse the repository at this point in the history

  5. Add a utility function in AstUtils to go from the old representation … 

    …of cases to the new one
    @mattam82
    mattam82 committed Jan 27, 2021
    Configuration menu
    Copy the full SHA
    309a3f5 View commit details
    Browse the repository at this point in the history

  6. All plugins compile

    @mattam82
    mattam82 committed Jan 27, 2021
    Configuration menu
    Copy the full SHA
    22cfd3f View commit details
    Browse the repository at this point in the history

  7. Add monad_utils as a dependency to the template monad plugin (useful … 

    …to write partial functions)
    @mattam82
    mattam82 committed Jan 27, 2021
    Configuration menu
    Copy the full SHA
    fcae1e0 View commit details
    Browse the repository at this point in the history

  8. Adapted translations (todo in param_original, wrong on case and induc… 

    …tives)
    @mattam82
    mattam82 committed Jan 27, 2021
    Configuration menu
    Copy the full SHA
    4a97025 View commit details
    Browse the repository at this point in the history

  9. Add convenience constructors in AstUtils for building inductive and c… 

    …onstructor bodies without redundant information
    @mattam82
    mattam82 committed Jan 27, 2021
    Configuration menu
    Copy the full SHA
    16c25e5 View commit details
    Browse the repository at this point in the history

  10. Fix the test-suite, and improve Pretty to print environments

    @mattam82
    mattam82 committed Jan 27, 2021
    Configuration menu
    Copy the full SHA
    ccecc44 View commit details
    Browse the repository at this point in the history

  11. Fix test-suite scripts

    @mattam82
    mattam82 committed Jan 27, 2021
    Configuration menu
    Copy the full SHA
    6f81b2c View commit details
    Browse the repository at this point in the history

  12. A bug revealed by the safe checker, probably in reification

    @mattam82
    mattam82 committed Jan 27, 2021
    Configuration menu
    Copy the full SHA
    ebde62a View commit details
    Browse the repository at this point in the history

Commits on Jan 28, 2021

  1. Fix an order bug in iota_red! The arguments where substituted in the … 

    …wrong order...
    @mattam82
    mattam82 committed Jan 28, 2021
    Configuration menu
    Copy the full SHA
    fdbb0c6 View commit details
    Browse the repository at this point in the history

  2. Params were substituted in the wrong order in case contexts too, fixed

    @mattam82
    mattam82 committed Jan 28, 2021
    Configuration menu
    Copy the full SHA
    c34dbb8 View commit details
    Browse the repository at this point in the history

  3. Better printer for type-checking/conversion errors

    @mattam82
    mattam82 committed Jan 28, 2021
    Configuration menu
    Copy the full SHA
    f571a5e View commit details
    Browse the repository at this point in the history

  4. SafeChecker tests passing again

    @mattam82
    mattam82 committed Jan 28, 2021
    Configuration menu
    Copy the full SHA
    dfb9f4a View commit details
    Browse the repository at this point in the history

  5. Finally everything compiles

    @mattam82
    mattam82 committed Jan 28, 2021
    Configuration menu
    Copy the full SHA
    51ba714 View commit details
    Browse the repository at this point in the history

  6. Finish safe reduction

    @jakobbotsch
    jakobbotsch committed Jan 28, 2021
    Configuration menu
    Copy the full SHA
    a3c3a5f View commit details
    Browse the repository at this point in the history

  7. New ctx_inst hypothesis in Typing

    @mattam82
    mattam82 committed Jan 28, 2021
    Configuration menu
    Copy the full SHA
    fc66073 View commit details
    Browse the repository at this point in the history

Commits on Jan 29, 2021

  1. Finished validity proof

    @mattam82
    mattam82 committed Jan 29, 2021
    Configuration menu
    Copy the full SHA
    6151fe9 View commit details
    Browse the repository at this point in the history

  2. Also include the (derivable) consistent_instance_ext hyp in cases for… 

    … uniformity.
    @mattam82
    mattam82 committed Jan 29, 2021
    Configuration menu
    Copy the full SHA
    cabe334 View commit details
    Browse the repository at this point in the history

  3. Renaming of validity_term to validity

    @mattam82
    mattam82 committed Jan 29, 2021
    Configuration menu
    Copy the full SHA
    f8ddf7c View commit details
    Browse the repository at this point in the history

Commits on Feb 1, 2021

  1. Update PCUICSafeLemmata, various refactorings

    @jakobbotsch
    jakobbotsch committed Feb 1, 2021
    Configuration menu
    Copy the full SHA
    19eae80 View commit details
    Browse the repository at this point in the history

  2. Add a lemma relating typing_spine and ctx_inst

    @mattam82
    mattam82 committed Feb 1, 2021
    Configuration menu
    Copy the full SHA
    6866edc View commit details
    Browse the repository at this point in the history

Commits on Feb 2, 2021

  1. Prove lemmas showing ctx_inst plays well with cumulativity of inducti… 

    …ve types
    @mattam82
    mattam82 committed Feb 2, 2021
    Configuration menu
    Copy the full SHA
    836228f View commit details
    Browse the repository at this point in the history

Commits on Feb 5, 2021

  1. Update safe conversion for new representation 

    Also changes stacks to use lists.
    @jakobbotsch
    jakobbotsch committed Feb 5, 2021
    Configuration menu
    Copy the full SHA
    68cff52 View commit details
    Browse the repository at this point in the history

Commits on Feb 8, 2021

  1. Some cleanup

    @jakobbotsch
    jakobbotsch committed Feb 8, 2021
    Configuration menu
    Copy the full SHA
    269313f View commit details
    Browse the repository at this point in the history

  2. Fix error

    @jakobbotsch
    jakobbotsch committed Feb 8, 2021
    Configuration menu
    Copy the full SHA
    9e5392d View commit details
    Browse the repository at this point in the history

Commits on Feb 9, 2021

  1. Update case inversion data and fix some todos

    @jakobbotsch
    jakobbotsch committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    3a6d451 View commit details
    Browse the repository at this point in the history

  2. Shorten some lemmas in Sigma-Calculus using the algebraic identities

    @mattam82
    mattam82 committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    54b814b View commit details
    Browse the repository at this point in the history

  3. Move subst_consn_lt' to sigma calculus

    @mattam82
    mattam82 committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    3487e11 View commit details
    Browse the repository at this point in the history

  4. Simplify closed_subst_map_lift proof using sigma-calculus instead of … 

    …brute-force induction
    @mattam82
    mattam82 committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    ed91b57 View commit details
    Browse the repository at this point in the history

  5. Minor refactorings in sigma-calculus proofs

    @mattam82
    mattam82 committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    fabaaed View commit details
    Browse the repository at this point in the history

  6. WIP in inductive inversion

    @mattam82
    mattam82 committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    223b5f2 View commit details
    Browse the repository at this point in the history

  7. WIP in typing of branches still.

    @mattam82
    mattam82 committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    8e88469 View commit details
    Browse the repository at this point in the history

  8. Fix duplication in conversion, and add missing injectivity of product… 

    …s for conversion
    @mattam82
    mattam82 committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    8560127 View commit details
    Browse the repository at this point in the history

  9. Finally finished build_branches_types_wt proof, using more general le… 

    …mmas for spines involving identity substitutions
    @mattam82
    mattam82 committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    ce09486 View commit details
    Browse the repository at this point in the history

  10. PCUICEqualityDec moved to PCUIC for now

    @mattam82
    mattam82 committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    6ccd915 View commit details
    Browse the repository at this point in the history

  11. finish aux lemma and cleanup PCUICInductiveInversion

    @mattam82
    mattam82 committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    a9fc669 View commit details
    Browse the repository at this point in the history

  12. Fix broken install of template-coq as some files are no longer needed

    @mattam82
    mattam82 committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    364f8ee View commit details
    Browse the repository at this point in the history

  13. More fixes for the safechecker and erasure plugins

    @mattam82
    mattam82 committed Feb 9, 2021
    Configuration menu
    Copy the full SHA
    5fbcc40 View commit details
    Browse the repository at this point in the history

Commits on Feb 10, 2021

  1. WIP in SR, much simpler now

    @mattam82
    mattam82 committed Feb 10, 2021
    Configuration menu
    Copy the full SHA
    5daa2f6 View commit details
    Browse the repository at this point in the history

  2. Before trying subst_app_simpl instead

    @mattam82
    mattam82 committed Feb 10, 2021
    Configuration menu
    Copy the full SHA
    31ca371 View commit details
    Browse the repository at this point in the history

Commits on Feb 11, 2021

  1. Finished and cleaned up iota reduction type preservation

    @mattam82
    mattam82 committed Feb 11, 2021
    Configuration menu
    Copy the full SHA
    c3e2da3 View commit details
    Browse the repository at this point in the history

  2. Checked that congruence for params can be proved without changing the… 

    … spec
    @mattam82
    mattam82 committed Feb 11, 2021
    Configuration menu
    Copy the full SHA
    75393b0 View commit details
    Browse the repository at this point in the history

  3. Fix typing rule for SR (equivalent under context conversion)

    @mattam82
    mattam82 committed Feb 11, 2021
    Configuration menu
    Copy the full SHA
    bb333db View commit details
    Browse the repository at this point in the history

Commits on Feb 12, 2021

  1. Almost done in SR, only a refactoring is needed to avoid duplication,… 

    … but all cases on case are done
    @mattam82
    mattam82 committed Feb 12, 2021
    Configuration menu
    Copy the full SHA
    48e75f8 View commit details
    Browse the repository at this point in the history

  2. Refactored wf_case_branches_types for reuse in SR proof

    @mattam82
    mattam82 committed Feb 12, 2021
    Configuration menu
    Copy the full SHA
    fab0cae View commit details
    Browse the repository at this point in the history

  3. Finished Subject Reduction for cases!

    @mattam82
    mattam82 committed Feb 12, 2021
    Configuration menu
    Copy the full SHA
    8d1c85d View commit details
    Browse the repository at this point in the history

Commits on Feb 13, 2021

  1. Admit free subject reduction proof

    @mattam82
    mattam82 committed Feb 13, 2021
    Configuration menu
    Copy the full SHA
    8b06578 View commit details
    Browse the repository at this point in the history

  2. Refactorings to finish PCUICAlpha

    @mattam82
    mattam82 committed Feb 13, 2021
    Configuration menu
    Copy the full SHA
    f748140 View commit details
    Browse the repository at this point in the history

  3. Refactor proofs so that alpha-conversion is not needed for PCUICInduc… 

    …tiveInversion
    @mattam82
    mattam82 committed Feb 13, 2021
    Configuration menu
    Copy the full SHA
    c2167f0 View commit details
    Browse the repository at this point in the history

Commits on Feb 14, 2021

  1. Complete alpha-conversion proof

    @mattam82
    mattam82 committed Feb 14, 2021
    Configuration menu
    Copy the full SHA
    aeab3a6 View commit details
    Browse the repository at this point in the history

  2. Cleaned up notations in PCUICAlpha, move generic lemmas up

    @mattam82
    mattam82 committed Feb 14, 2021
    Configuration menu
    Copy the full SHA
    5c3255f View commit details
    Browse the repository at this point in the history

  3. More move of generic lemmas back in the prelude

    @mattam82
    mattam82 committed Feb 14, 2021
    Configuration menu
    Copy the full SHA
    32b9b75 View commit details
    Browse the repository at this point in the history

Commits on Feb 15, 2021

  1. Minor refactorings

    @mattam82
    mattam82 committed Feb 15, 2021
    Configuration menu
    Copy the full SHA
    69f7030 View commit details
    Browse the repository at this point in the history

  2. Fill TODOs in CumulProp and Principality.

    @mattam82
    mattam82 committed Feb 15, 2021
    Configuration menu
    Copy the full SHA
    9e4600e View commit details
    Browse the repository at this point in the history

Commits on Feb 16, 2021

  1. Remove all TODOs in WfUniverse

    @mattam82
    mattam82 committed Feb 16, 2021
    Configuration menu
    Copy the full SHA
    7547aac View commit details
    Browse the repository at this point in the history

  2. No more todos in PCUIC except for the correctness proofs of translations

    @mattam82
    mattam82 committed Feb 16, 2021
    Configuration menu
    Copy the full SHA
    853b6c5 View commit details
    Browse the repository at this point in the history

  3. Cleanup PCUICElimination, removing old proofs

    @mattam82
    mattam82 committed Feb 16, 2021
    Configuration menu
    Copy the full SHA
    876c0aa View commit details
    Browse the repository at this point in the history

  4. Fix script in canonicity, len is more robust now

    @mattam82
    mattam82 committed Feb 16, 2021
    Configuration menu
    Copy the full SHA
    01dcee1 View commit details
    Browse the repository at this point in the history

  5. Fix script

    @mattam82
    mattam82 committed Feb 16, 2021
    Configuration menu
    Copy the full SHA
    f936a16 View commit details
    Browse the repository at this point in the history

  6. Definition of weak-head-reduction and proof of unicity of derivations

    @mattam82
    mattam82 committed Feb 16, 2021
    Configuration menu
    Copy the full SHA
    06f8089 View commit details
    Browse the repository at this point in the history