Require Import Arith.

(** * Subtleties of dependent type theory *)

(** ** Classical reasoning *)

Lemma contra (P Q : Prop) : (Q -> P) -> ~ P -> ~ Q.
Proof.
  intros Himpl Hp.
  intros Hq.
  apply Hp, Himpl, Hq.
Qed.

Lemma dn_intro (P : Prop) : P -> ~~P.
Proof.
  intros Hp Hneg.
  apply Hneg, Hp.
Qed.

Lemma dn_elim (P : Prop) : ~~ P -> P.
Proof.
  intros Hp.
Abort.

Definition fermat : Prop := forall (n i j k : nat),
  3 <= n -> (i^n = j^n + k^n -> i = 0).

Lemma fermat_not : fermat \/ ~ fermat.
Proof.
  (* ???? *)
Abort.

Lemma fermat_from_dn : (forall P, ~~ P -> P) -> fermat \/ ~ fermat.
Proof.
  intros dneg.
  apply dneg.
  intros Hf.
  apply Hf.
  right.
  intros Hf'.
  apply Hf.
  left.
  assumption.
Qed.

(** Still sometimes provable *)

Lemma boolean_dec (P : Prop) (b : bool) :
  (P <-> (b = true)) ->
  P \/ ~ P.
Proof.
  intros HP.
  destruct b.
  - left.
    apply HP.
    reflexivity.
  - right.
    intros Hp.
    apply HP in Hp.
    discriminate Hp.
Qed.

Require Import Classical.

About classic.
About NNPP.

Lemma fermat_not : fermat \/ ~ fermat.
Proof.
  apply classic.
Defined.

Print Assumptions fermat_not.
Compute fermat_not. (* lost canonicity/constructivity *)

(** ** Functional extensionality *)

Lemma funext (A B : Type) (f g : A -> B) :
  (forall x, f x = g x) ->
  f = g.
Proof.
  intros.
Abort.

Require Import FunctionalExtensionality.

About functional_extensionality.

Lemma funext (A B : Type) (f g : A -> B) :
  (forall x, f x = g x) ->
  f = g.
Proof.
  intros.
  apply functional_extensionality.
  assumption.
Qed.

(** Incompatible with quoting and synthetic computability: *)

Axiom quote : (nat -> nat) -> nat.

(** Cf for instance https://github.com/uds-psl/coq-library-undecidability *)

(** ** Proof irrelevance *)

Check Prop.
Print or.

Fail Definition or_to_bool {P : Prop} (p : P \/ ~ P) : bool :=
  match p with
  | or_introl p => true
  | or_intror np => false
  end.

Definition plus_to_bool {A B : Type} (p : A + B) : bool :=
  match p with
  | inl p => true
  | inr p => false
  end.

(** Also useful for extraction *)

Lemma proof_irrel_fun (P : Prop) (A : Type) (f : P -> A) :
  forall x y : P, f x = f y.
Proof.
Abort.

(** Still sometimes provable *)

Require Import Eqdep_dec.

Require Import ProofIrrelevance.

About proof_irrelevance.

Lemma proof_irrel_fun (P : Prop) (A : Type) (f : P -> A) :
  forall x y : P, f x = f y.
Proof.
  intros x y.
  f_equal.
  apply proof_irrelevance.
Qed.

About UIP_dec.


(** UIP is incompatible with univalence *)
(** See Homotopy Type Theory *)

(** Summing up:
  - generally “underspecified” logic
  - opens the possibility for various non-standard principles, very useful for synthetic mathematics
  - can be repaired to go more towards “standard” mathematics with global assumptions
  - or by locally tracking the global assumptions as extra properties
*)