Stream: MetaCoq

Topic: adding False to Σ

view this post on Zulip Jason Gross (Nov 24 2022 at 00:07):

How would I go about proving

  forall cf : checker_flags,
  normalizing_flags ->
  forall (guard : abstract_guard_impl) (_Σ : referenced_impl_ext),
  axiom_free _Σ ->
  let Σ := referenced_impl_env_ext _Σ in
  let Σ' := global_env_add Σ.1 (make_fresh_name Σ, InductiveDecl False_mib) in
  let Σext := (Σ', Σ.2) in
  wf_ext Σext ->
  (forall (Γ : context) (t : term), welltyped _Σ Γ t -> Acc (cored _Σ Γ) t) ->
  forall (Γ : context) (t : term), welltyped Σext Γ t -> Acc (cored Σext Γ) t

without assuming normalisation? (Unqualified definitions are located as they would be if this were to be inserted as a goal at the end of safechecker/theories/PCUICConsistency.v)

Last updated: Jun 10 2023 at 06:31 UTC