3
$\begingroup$

Is it possible to prove the following theorem without axioms in Coq? Or is the following theorem equivalent to any well known axioms?

Theorem eq_dep_app: forall input (output1 output2: input -> Type) f1 f2,
  eq_dep Type id (forall i, output1 i) f1 (forall i, output2 i) f2 ->
  forall i, eq_dep Type id (output1 i) (f1 i) (output2 i) (f2 i).

I tried the following:

  intros.
  apply eq_dep_eq_sigT in H.
  apply eq_sigT_eq_dep.
  set (s1:= existT id (forall i : input, output1 i) f1) in *.
  set (s2:= existT id (forall i : input, output2 i) f2) in *.
  change f1 with (projT2 s1).
  change f2 with (projT2 s2).
  rewrite H.

However, the last rewrite tactic fails:

Abstracting over the term "s1" leads to a term
fun s0 : {x : Type & id x} =>
existT id (output1 i) (projT2 s0 i) = existT id (output2 i) (projT2 s2 i)
which is ill-typed.
Reason is: Illegal application (Non-functional construction):
The expression "projT2" of type
 "forall (A : Type) (P : A -> Type) (x : {x : A & P x}), P (projT1 x)"
cannot be applied to the terms
 "Type" : "Type"
 "id" : "Type -> Type"
 "s0" : "{x : Type & id x}"
 "i" : "input"

I interpret the error message as meaning that as part of rewriting projT2 s1 i (used to be f1 i) to projT2 s2 i (used to be f2 i), the rewrite tactic has to generalize s1 along with its type. As part of generalizing s1's type, it forgets that projT2 s1 is a function, which causes projT2 s1 i to no longer type check.

I know that the rewrite would work if I could replace all of the goal's references to f1 and output1 with something projected from s1, but I can't figure out a way to replace the references to output1.

$\endgroup$
2
  • 2
    $\begingroup$ Can you please include enough context that your code compiles? For example, what are you importing? $\endgroup$
    – Ana Borges
    Commented Mar 18, 2022 at 11:32
  • $\begingroup$ I would guess that it requires some sort of function extensionality. But I can't be sure without further info. $\endgroup$
    – Trebor
    Commented Mar 18, 2022 at 13:16

1 Answer 1

5
$\begingroup$

Assuming you're using EqDepFacts (https://coq.inria.fr/library/Coq.Logic.EqdepFacts.html).

You can prove some form of injectivity of of pi-types for propositional equality from your proposition.

From Coq Require Import EqdepFacts Utf8.

Theorem eq_dep_app :
  ∀ input (output1 output2 : input → Type) f1 f2,
    eq_dep Type (λ x, x) (∀ i, output1 i) f1 (∀ i, output2 i) f2 →
    ∀ i, eq_dep Type (λ x, x) (output1 i) (f1 i) (output2 i) (f2 i).
Admitted.

Corollary foo :
  @eq Type (nat → nat) (nat → bool) →
  @eq Type nat bool.
Proof.
  intro e.
  pose (f := λ x : nat, x).
  pose (g := @eq_rect Type (nat → nat) (λ x : Type, x) f (nat → bool) e).
  assert (e' : eq_dep Type (λ x, x) (nat → bool) g (nat → nat) f).
  { apply eq_dep1_dep. exists e. reflexivity. }
  apply eq_dep_app with (i := 0) in e'.
  apply eq_dep_dep1 in e'.
  destruct e'.
  assumption.
Qed.

The cardinal model of type theory validates (nat → nat) = (nat → bool) but not nat = bool so your proposition is not provable.

$\endgroup$
2
  • $\begingroup$ In the cardinal model your corollary is simply false, right? If so it is definitely not provable, and so the theorem also is. $\endgroup$ Commented Mar 18, 2022 at 15:50
  • 1
    $\begingroup$ Indeed, this is what I meant. Maybe I should say it more strongly. $\endgroup$ Commented Mar 18, 2022 at 16:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.