Stream: MetaCoq

Topic: `type_mkApps`


view this post on Zulip Jason Gross (Apr 14 2023 at 20:51):

I see type_mkApps in PCUICSpine, is there an equivalent lemma proven for template typing? If not, how should I prove it, and which file does it belong in? (Right now, I have

Lemma type_mkApps {cf : checker_flags} {Σ Γ t u T t_ty} :
  (Σ ;;; Γ |- t : t_ty) ->
  typing_spine Σ Γ t_ty u T ->
  Σ ;;; Γ |- mkApps t u : T.
Proof.
  destruct 2; cbn; trivial.
  destruct ?; subst.
  all: try solve [ do 3 try first [ eassumption
                                  | reflexivity
                                  | congruence
                                  | econstructor ] ];
    [ > ].
  match goal with
  | [ H : _;;; _ |- tApp ?f ?x : _ |- _ ;;; _ |- tApp ?f (?x ++ _) : _ ]
    => inversion H; subst
  end.
  { econstructor; try eassumption; try congruence.
    { match goal with |- ?x ++ _ :: _ <> [] => now destruct x end. }
    { shelve. (* ???
1 goal (ID 8037)

  cf : checker_flags
  Σ : global_env_ext
  Γ : context
  T, t2 : term
  args : list term
  X : Σ;;; Γ |- tApp t2 args : T
  hd : term
  tl : list term
  na : aname
  A, B : term
  s : Universe.t
  B' : term
  t0 : Σ;;; Γ |- tProd na A B : tSort s
  c : Σ;;; Γ |- T <= tProd na A B
  t1 : Σ;;; Γ |- hd : A
  X0 : typing_spine Σ Γ (B {0 := hd}) tl B'
  t_ty : term
  X1 : Σ;;; Γ |- t2 : t_ty
  H1 : isApp t2 = false
  H3 : args <> []
  X2 : typing_spine Σ Γ t_ty args T
  ============================
  typing_spine Σ Γ t_ty (args ++ hd :: tl) B'
 *) } }
  { econstructor; try eassumption; [ | | ].
    (* ???
3 focused goals (shelved: 3) (ID 11491)

  cf : checker_flags
  Σ : global_env_ext
  Γ : context
  T, t2 : term
  args : list term
  X : Σ;;; Γ |- tApp t2 args : T
  hd : term
  tl : list term
  na : aname
  A, B : term
  s : Universe.t
  B' : term
  t0 : Σ;;; Γ |- tProd na A B : tSort s
  c : Σ;;; Γ |- T <= tProd na A B
  t1 : Σ;;; Γ |- hd : A
  X0 : typing_spine Σ Γ (B {0 := hd}) tl B'
  A0 : term
  s0 : Universe.t
  X1 : Σ;;; Γ |- tApp t2 args : A0
  X2 : Σ;;; Γ |- T : tSort s0
  X3 : Σ;;; Γ |- A0 <= T
  ============================
  Σ;;; Γ |- tApp t2 (args ++ hd :: tl) : ?A

goal 2 (ID 11492) is:
 Σ;;; Γ |- B' : tSort ?s
goal 3 (ID 11493) is:
 Σ;;; Γ |- ?A <= B'
*)

and I'm kinda stuck)

view this post on Zulip Matthieu Sozeau (Apr 17 2023 at 07:26):

It should be an induction on the typing spine/u


Last updated: Jul 23 2024 at 20:01 UTC