Function good_proof_irrelevance

crates/kernel/src/tutorial/defeq.rs:18–57

()

  /// proofIrrelevance : ∀ (p : Prop) (h1 h2 : p), h1 = h2 := fun _ _ _ => rfl
  #[test]
  fn good_proof_irrelevance() {
    let mut env = KEnv::<Meta>::new();
    add_eq_axioms(&mut env);

    // ∀ (p : Prop) (h1 h2 : p), Eq.{0} p h1 h2
    // depth 3: p=var(2), h1=var(1), h2=var(0)
    let ty = npi(
      "p",
      sort0(),
      npi(
        "h1",
        var(0),
        npi("h2", var(1), eq_expr(uzero(), var(2), var(1), var(0))),
      ),
    );

    // fun p h1 h2 => Eq.refl.{0} p h1
    // Eq.refl h1 : Eq h1 h1, but declared type says Eq h1 h2.
    // Proof irrelevance makes h1 = h2 since both : p (a Prop).
    let val = nlam(
      "p",
      sort0(),
      nlam(
        "h1",
        var(0),
        nlam("h2", var(1), eq_refl_expr(uzero(), var(2), var(1))),
      ),
    );

    let (id, c) = mk_defn(
      "proofIrrelevance",
      0,
      vec![],
      ty,
      val,
      ix_common::env::ReducibilityHints::Abbrev,
    );
    env.insert(id.clone(), c);
    check_accepts(&mut env, &id);
  }

  /// funEta : ∀ (α β : Type) (f : α → β), (fun x => f x) = f := fun _ _ f => rfl
  #[test]