LogRel.Consequences: important meta-theoretic consequences of normalization: canonicity of natural numbers and consistency.

From Coq Require Import CRelationClasses.
From LogRel.AutoSubst Require Import core unscoped Ast Extra.
From LogRel Require Import Utils BasicAst Notations Context NormalForms Weakening UntypedReduction
  LogicalRelation Fundamental Validity LogicalRelation.Induction Substitution.Escape LogicalRelation.Irrelevance
  GenericTyping DeclarativeTyping DeclarativeInstance TypeConstructorsInj Normalisation.

Import DeclarativeTypingData DeclarativeTypingProperties.

Lemma no_neutral_empty_ctx {A t} : whne t -> [ε |-[de] t : A] -> False.
Proof.
  intros wh; induction wh in A |- *.
  - intros [? [[? [?? h]]]]%termGen'; inversion h.
  - intros [? [[? [? []]]]]%termGen'; eauto.
  - intros [? [[? []]]]%termGen'; eauto.
  - intros [? [[? []]]]%termGen'; eauto.
  - intros [? [[? [? []]]]]%termGen'; eauto.
  - intros [? [[? [? []]]]]%termGen'; eauto.
  - intros [? [[?]]]%termGen'; eauto.
Qed.

Lemma wty_norm {Γ t A} : [Γ |- t : A] ->
  ∑ wh, [× whnf wh, [Γ |- t ⤳* wh : A]& [Γ |- wh : A]].
Proof.
  intros wtyt.
  pose proof (normalisation wtyt) as [wh red].
  pose proof (h := subject_reduction _ _ _ _ wtyt red).
  assert [Γ |- wh : A] by (destruct h; boundary).
  now eexists.
Qed.

Lemma consistency {t} : [ε |- t : tEmpty] -> False.
Proof.
  intros [wh []]%wty_norm; refold.
  eapply no_neutral_empty_ctx; tea.
  eapply empty_isEmpty; tea.
Qed.

Print Assumptions consistency.

Section NatCanonicityInduction.

  Let numeral : nat -> term := fun n => Nat.iter n tSucc tZero.

  #[local] Coercion numeral : nat >-> term.

  #[local] Lemma red_nat_empty : [ε ||-Nat tNat].
  Proof.
    repeat econstructor.
  Qed.

  Lemma nat_red_empty_ind :
    (forall t, [ε ||-Nat t : tNat | red_nat_empty] ->
    ∑ n : nat, [ε |- t ≅ n : tNat]) ×
    (forall t, NatProp red_nat_empty t -> ∑ n : nat, [ε |- t ≅ n : tNat]).
  Proof.
    apply NatRedInduction.
    - intros * [? []] ? _ [n] ; refold.
      exists n.
      now etransitivity.
    - exists 0 ; cbn.
      now repeat constructor.
    - intros ? _ [n].
      exists (S n) ; simpl.
      now econstructor.
    - intros ? [? [? _ _]].
      exfalso.
      now eapply no_neutral_empty_ctx.
  Qed.

  Lemma _nat_canonicity {t} : [ε |- t : tNat] ->
  ∑ n : nat, [ε |- t ≅ n : tNat].
  Proof.
    intros Ht.
    assert [LRNat_ one red_nat_empty | ε ||- t : tNat] as ?%nat_red_empty_ind.
    {
      apply Fundamental in Ht as [?? Vt%reducibleTm].
      irrelevance.
    }
    now assumption.
  Qed.

End NatCanonicityInduction.

Lemma nat_canonicity {t} : [ε |- t : tNat] ->
  ∑ n : nat, [ε |- t ≅ Nat.iter n tSucc tZero : tNat].
Proof.
  now apply _nat_canonicity.
Qed.