Stream: MetaCoq

Topic: generalizing from typing in the empty context


view this post on Zulip Jason Gross (Apr 14 2023 at 21:06):

Is there a lemma that shows (Σ;;; [] |- t : T) -> (Σ;;; Γ |- t : T) (notably, there's no need to subst on closed terms)?

view this post on Zulip Yannick Forster (Apr 14 2023 at 21:24):

Weakening gives you this, but will have a lift on closed terms

view this post on Zulip Jason Gross (Apr 14 2023 at 21:28):

Is there a lemma that lets me get rid of the lift?

view this post on Zulip Jason Gross (Apr 14 2023 at 21:39):

(The thing I'm trying to prove right now is

   forall Γ : context,
  wf_local Σ Γ ->
  Σ;;; [] |- qP
  : tSort
      (Universe.lType
         {|
           t_set :=
             {|
               LevelExprSet.this := [(Level.level "MetaCoq.Quotation.ToPCUIC.Init.Typing.547", 0)];
               LevelExprSet.is_ok := LevelExprSet.Raw.singleton_ok (Level.level "MetaCoq.Quotation.ToPCUIC.Init.Typing.547", 0)
             |};
           t_ne := eq_refl
         |}) ->
  Σ;;; [] |- qH
  : tProd {| binder_name := nAnon; binder_relevance := Relevant |}
      (tApp
         (tApp
            (tApp (tInd {| inductive_mind := (MPfile ["Logic"; "Init"; "Coq"], "eq"); inductive_ind := 0 |} [])
               (tInd {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "bool"); inductive_ind := 0 |} []))
            (tConstruct {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "bool"); inductive_ind := 0 |} 0 []))
         (tConstruct {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "bool"); inductive_ind := 0 |} 0 [])) qP ->
  Σ;;; Γ
  |- tApp qH
       (tApp
          (tApp (tConstruct {| inductive_mind := (MPfile ["Logic"; "Init"; "Coq"], "eq"); inductive_ind := 0 |} 0 [])
             (tInd {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "bool"); inductive_ind := 0 |} []))
          (tConstruct {| inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "bool"); inductive_ind := 0 |} 0 [])) : qP

subject to appropriate constraints on Σ. Basically if I have that qP is a type and qH : true = true -> qP, both in the empty context, then I can type qH (eq_refl true) : qP in any context.

view this post on Zulip Yannick Forster (Apr 14 2023 at 21:43):

Well, lifting a closed term is equivalent to a term, but I guess you don't want that?

view this post on Zulip Yann Leray (Apr 14 2023 at 21:58):

Lemma lift_closed n k t : closedn k t -> lift n k t = t. ?


Last updated: Jul 23 2024 at 21:01 UTC