Coq練習問題(2)

coq2.v

Require Import ssreflect.
Section Coq3.
  Variable A : Set.
  Variable R : A -> A -> Prop.
  Variable P Q : A -> Prop.

  Theorem exists_postpone : (exists x, forall y, R x y) -> (forall y, exists x, R x y).
  Proof.
    move => [ea] y.
    move => y0.
    specialize (y y0).
    exists ea.
    assumption.
    
  Qed.
  

  Theorem or_exists_postpone : (exists x, P x) \/ (exists x, Q x) -> exists x, P x \/ Q x.
  Proof.
    move => [[e1]|[e2]].
    + move => p.
      exists e1.
      left.
      assumption.
    + move => q.
      exists e2.
      right.
      assumption.
  Qed.

  Hypothesis classic : forall P, ~ ~ P -> P.
  (*Theorem exclusive : forall P, P \/ ~P.
  Proof.
    move => P0.
    apply (classic (P0 \/ ~ P0)).
    move => n_pnp.
    
    
  Qed.
  Theorem peirce_law : forall (P Q : Prop), ((P -> Q) -> P) -> P.
  Proof.
    move => p q pqp.
    apply (classic p).
    move => np.
    
    
    
  Qed.
  Theorem remove_c : forall a,
    (forall x y, Q x -> Q y) -> (forall c, ((exists x, P x) -> P c) -> Q c) -> Q a.
    Proof.
      move => a qxqy hyp.
      cut ((forall x y, Q x -> Q y) -> (forall y1 x1, Q x1 -> Q y1)).
      Abort.
      
      
    (* Qed.*)

  Theorem remove_c2 : forall a,
    (forall y x, Q x -> Q y) -> (forall c, ((exists x, P x) -> P c) -> Q c) -> Q a.
    Proof.
      move => a qxqy hyp.
      specialize (qxqy a).
      
      
      
      
    Qed.*)
End Coq3.


Section SystemF. 
Definition Fand P Q := forall X : Prop, (P -> Q -> X) -> X. 
Definition For P Q := forall X : Prop, (P -> X) -> (Q -> X) -> X. 
Definition Ffalse := forall X : Prop, X. 
Definition Ftrue := forall X : Prop, (X -> X).
Definition Feq T (x y : T) := forall P, P x <-> P y. 
Definition Fex T (P : T -> Prop) := forall X : Prop, (forall x, P x -> X) -> X.
Theorem Fand_ok (P Q : Prop) : Fand P Q <-> P /\ Q. Proof.
  rewrite /Fand.
  split.
  + move => fver.
    specialize (fver (P /\ Q)).
    apply fver.
    move => p q.
    split.
    assumption.
    assumption.
  + move => [p q].
    move => x pqx.
    apply pqx.
    assumption.
    assumption.
Qed.
Theorem For_ok (P Q : Prop) : For P Q <-> P \/ Q.
Proof.
  rewrite /For.
  split.
  + move => fver.
    specialize (fver (P\/Q)).
    apply fver.
    - move => p.
      left.
      assumption. 
    - move => q.
      right.
      assumption.
  + move => [p|q] x px qx.
    - apply px.
      assumption.
    - apply qx.
      assumption.
Qed.
Theorem Ffalse_ok : Ffalse <-> False.
Proof.
  rewrite /Ffalse.
  split.
  + move => asm.
    specialize (asm False).
    assumption.
  + move => f.
    exfalso.
    assumption.
Qed.
Theorem Ftrue_ok : Ftrue <-> True.
Proof.
  rewrite /Ftrue.
  split.
  + move => fver.
    done.
  + move => cver x asm.
    assumption.
Qed.
Theorem Feq_ok T (x y : T) : Feq T x y <-> x = y.
Proof.
  rewrite /Feq.
  split.
  + move => fver.
    specialize (fver (eq x)).
    move: fver.
    move => [xx xy].
    apply xx.
    reflexivity.
  + move => qver t.
    split.
    - move => tx.
      rewrite <- qver.
      assumption.
    - move => ty.
      rewrite qver.
      assumption.
Qed.

Theorem Fex_ok T (P : T -> Prop) : Fex T P <-> exists x, P x. 
Proof.
  rewrite /Fex.
  split.
  + move => fver.
    specialize (fver (exists x, P x)).
    apply fver.
    move => x px.
    exists x.
    assumption.
  + move => [qver] px x all. 
    specialize (all qver).
    apply all.
    assumption.
Qed.

End SystemF.