Library eq_rel


Require Export universe.

Inductive void : [univ] := .



Inductive t_iff (A B : [univ]) : [univ] :=
 | t_iff_cons : (AB) → (BA) → t_iff A B.

Notation "x <=> y" := (t_iff x y) (at level 95, no associativity).

Lemma tiff_trans :
   a b c, (a <=> b) → (b <=> c) → (a <=> c).
Proof.
  intros a b c i1 i2.
  destruct i1 as [i11 i12].
  destruct i2 as [i21 i22].
  split; intro k.
  apply i11 in k; apply i21 in k; auto.
  apply i22 in k; apply i12 in k; auto.
Qed.

Ltac dtiff :=
  match goal with
      [ H : ?x <=> ?y |- _ ] ⇒ destruct H
  end.

Ltac dtiffs := repeat dtiff.

Ltac dprod :=
  match goal with
      [ H : ?x # ?y |- _ ] ⇒ destruct H
  end.

Ltac dprods := repeat dprod.

Ltac dsum :=
  match goal with
      [ H : ?x [+] ?y |- _ ] ⇒ destruct H
  end.

Ltac dsums := repeat dsums.

Ltac dall :=
  repeat match goal with
           | [ H : ?x <=> ?y |- _ ] ⇒ destruct H
           | [ H : ?x # ?y |- _ ] ⇒ destruct H
           | [ H : ?x [+] ?y |- _ ] ⇒ destruct H
         end.

Definition tiff_fst :=
  fun {A B : [univ]} (p : A <=> B) ⇒ let (x, _) := p in x.

Definition tiff_snd :=
  fun {A B : [univ]} (p : A <=> B) ⇒ let (_, y) := p in y.

Lemma tiff_is_prod_implies1 :
   A B,
    (A <=> B) <=> ((AB) # (BA)).
Proof.
  intros; split; intros k; split; intros; destruct k; auto.
Qed.

Lemma tiff_is_prod_implies2 :
   A B : [univ],
    ((AB) # (BA)) <=> (A <=> B).
Proof.
  intros; split; intros k; split; intros; destruct k; auto.
Qed.

Lemma combine_t_iff_proofs_imp :
   {A B A' B' : [univ]},
    (A <=> A') → (B <=> B') → ((AB) <=> (A'B')).
Proof.
  intros; dall; constructor; auto.
Qed.

Lemma combine_t_iff_proofs_t_iff :
   {A B A' B'},
    (A <=> A')
    → (B <=> B')
    → ((A <=> B) <=> (A' <=> B')).
Proof.
  intros.
  dall; constructor; intro; dall; constructor; auto.
Qed.

Lemma combine_t_iff_proofs_prod :
   {A B A' B'},
    (A <=> A')
    → (B <=> B')
    → ((A # B) <=> (A' # B')).
Proof.
  intros.
  dall; constructor; intro; dall; auto.
Qed.

Lemma combine_t_iff_proofs_sum :
   {A B A' B'},
    (A <=> A')
    → (B <=> B')
    → ((A [+] B) <=> (A' [+] B')).
Proof.
  intros.
  dall; constructor; intro; dall; auto.
Qed.

Lemma combine_t_iff_proofs_not :
   {A A'},
    (A <=> A')
    → (!A <=> !A').
Proof.
  intros.
  dall; constructor; repeat intro; auto.
Qed.

Lemma t_iff_refl :
   A, A <=> A.
Proof.
  intros; constructor; auto.
Qed.

Lemma t_iff_sym :
   {A B}, (A <=> B) → (B <=> A).
Proof.
  intros.
  dall; constructor; auto.
Qed.

Ltac build_tiff_term T a b p :=
  match T with
    | ap
    | ?x → ?y
      let l := build_tiff_term x a b p in
      let r := build_tiff_term y a b p in
      constr:(combine_t_iff_proofs_imp l r)
    | ?x <=> ?y
      let l := build_tiff_term x a b p in
      let r := build_tiff_term y a b p in
      constr:(combine_t_iff_proofs_t_iff l r)
    | ?x # ?y
      let l := build_tiff_term x a b p in
      let r := build_tiff_term y a b p in
      constr:(combine_t_iff_proofs_prod l r)
    | ?x [+] ?y
      let l := build_tiff_term x a b p in
      let r := build_tiff_term y a b p in
      constr:(combine_t_iff_proofs_sum l r)
    | !?x
      let l := build_tiff_term x a b p in
      constr:(combine_t_iff_proofs_not l)
    | _constr:(t_iff_refl T)
  end.

Tactic Notation "thin_last" :=
  match goal with H: ?T |- _clear H end.

Ltac apply' H1 H2 :=
  let H3 := fresh in (
    (pose proof (H1 H2) as H3; clear H2; pose proof H3 as H2; clear H3) ||
    (pose proof (H1 _ H2) as H3; clear H2; pose proof H3 as H2; clear H3) ||
    (pose proof (H1 _ _ H2) as H3; clear H2; pose proof H3 as H2; clear H3) ||
    (pose proof (H1 _ _ _ H2) as H3; clear H2; pose proof H3 as H2; clear H3) ||
    (pose proof (H1 _ _ _ _ H2) as H3; clear H2; pose proof H3 as H2; clear H3)).

Ltac build_and_rewrite H :=
  let T := type of H in
  match goal with
    | [ |- ?C ] ⇒
      match T with
        | ?A <=> ?B
          let d := build_tiff_term C A B H in
          let name := fresh H in
          remember d as name;
            thin_last;
            apply name;
            clear name
      end
  end.

Ltac build_and_rewrite_hyp H H2 :=
  let T := type of H in
  let C := type of H2 in
  match T with
    | ?A <=> ?B
      let d := build_tiff_term C A B H in
      let name := fresh H in
      remember d as name;
        thin_last;
        apply' (tiff_fst name) H2;
        clear name
  end.

Ltac build_and_rewrite_rev H :=
  let T := type of H in
  match goal with
    | [ |- ?C ] ⇒
      match T with
        | ?A <=> ?B
          let d := build_tiff_term C B A (t_iff_sym H) in
          let name := fresh H in
          remember d as name;
            thin_last;
            apply name;
            clear name
      end
  end.

Ltac build_and_rewrite_hyp_rev H H2 :=
  let T := type of H in
  let C := type of H2 in
  match T with
    | ?A <=> ?B
      let d := build_tiff_term C B A (t_iff_sym H) in
      let name := fresh H in
      remember d as name;
        thin_last;
        apply' (tiff_fst name) H2;
        clear name
  end.

Tactic Notation "trewrite" ident(H) :=
       build_and_rewrite H.

Tactic Notation "trewrite" ident(H) "in" ident (H') :=
       build_and_rewrite_hyp H H'.

Tactic Notation "trewrite" "<-" ident(H) :=
       build_and_rewrite_rev H.

Tactic Notation "trewrite" "<-" ident(H) "in" ident(H') :=
       build_and_rewrite_hyp_rev H H'.

Ltac get_instance_of T H Hn :=
  match H with
    | _
     let name:= fresh "Htemp" in
      
     progress (
        (pose proof (fun h:H ⇒ (tiff_fst T) h) as name)||
        (pose proof (fun h:H ⇒ (tiff_fst (T _)) h) as name) ||
        (pose proof (fun h:H ⇒ (tiff_fst (T _ _)) h) as name) ||
        (pose proof (fun h:H ⇒ (tiff_fst (T _ _ _)) h) as name) ||
        (pose proof (fun h:H ⇒ (tiff_fst (T _ _ _ _)) h) as name) ||
        (pose proof (fun h:H ⇒ (tiff_fst (T _ _ _ _ _)) h) as name) ||
        (pose proof (fun h:H ⇒ (tiff_fst (T _ _ _ _ _ _)) h) as name) ||
        (pose proof (fun h:H ⇒ (tiff_fst (T _ _ _ _ _ _ _)) h) as name) ||
        (pose proof (fun h:H ⇒ (tiff_fst (T _ _ _ _ _ _ _ _)) h) as name)
      );
     let H2 := type of name in
         match H2 with
           | ?H → ?Hfail 1
           | ?H → ?H2
             clear name;
               assert (H <=> H2) as Hn by (apply T)
         
         end

    | ?Hl <=> ?Hrget_instance_of T Hl Hn || get_instance_of T Hr Hn
    | ?Hl # ?Hrget_instance_of T Hl Hn || get_instance_of T Hr Hn
    | ?Hl [+] ?Hrget_instance_of T Hl Hn || get_instance_of T Hr Hn
    | !?Hlget_instance_of T Hl Hn
    | ?Hl → ?Hrget_instance_of T Hl Hn || get_instance_of T Hr Hn
  end.

Ltac get_instance_of_rev T H Hn :=
  match H with
    | _
     let name:= fresh "Htemp" in
      
     progress (
        (pose proof (fun h:H ⇒ (tiff_snd T) h) as name)||
        (pose proof (fun h:H ⇒ (tiff_snd (T _)) h) as name) ||
        (pose proof (fun h:H ⇒ (tiff_snd (T _ _)) h) as name) ||
        (pose proof (fun h:H ⇒ (tiff_snd (T _ _ _)) h) as name) ||
        (pose proof (fun h:H ⇒ (tiff_snd (T _ _ _ _)) h) as name) ||
        (pose proof (fun h:H ⇒ (tiff_snd (T _ _ _ _ _)) h) as name) ||
        (pose proof (fun h:H ⇒ (tiff_snd (T _ _ _ _ _ _)) h) as name) ||
        (pose proof (fun h:H ⇒ (tiff_snd (T _ _ _ _ _ _ _)) h) as name) ||
        (pose proof (fun h:H ⇒ (tiff_snd (T _ _ _ _ _ _ _ _)) h) as name)
      );
     let H2 := type of name in
         match H2 with
           | ?H → ?Hfail 1
           | ?H → ?H2
             clear name;
               assert (H2 <=> H) as Hn by (apply T)
         
H2 in LHS; apply does not automatically take care of symmetry
         
         end

    | ?Hl <=> ?Hrget_instance_of_rev T Hl Hn || get_instance_of_rev T Hr Hn
    | ?Hl # ?Hrget_instance_of_rev T Hl Hn || get_instance_of_rev T Hr Hn
    | ?Hl [+] ?Hrget_instance_of_rev T Hl Hn || get_instance_of_rev T Hr Hn
    | !?Hlget_instance_of_rev T Hl Hn
    | ?Hl → ?Hrget_instance_of_rev T Hl Hn || get_instance_of_rev T Hr Hn
  end.

rewrite using a universally quantified t_iff relation T in the conclusion
Ltac trw T :=
  match goal with
      [ |- ?C ] ⇒
      let name:= fresh "Hget_instance_of_in_concl" in
      get_instance_of T C name;
        build_and_rewrite name; clear name
  end.

Ltac trw_rev T :=
  match goal with
      [ |- ?C ] ⇒
      let name:= fresh "Hget_instance_of_in_concl" in
      get_instance_of_rev T C name;
        build_and_rewrite_rev name ; clear name
  end.

Ltac trw_h T h :=
  let C := type of h in
  let name:= fresh "Hget_instance_of_in_concl" in
  get_instance_of T C name;
    build_and_rewrite_hyp name h; clear name.

Ltac trw_rev_h T h :=
  let C := type of h in
  let name:= fresh "Hget_instance_of_in_concl" in
  get_instance_of_rev T C name;
    build_and_rewrite_hyp_rev name h; clear name.


Tactic Notation "rw" constr(T) :=
  trw T || rewrite T.
Tactic Notation "rw" "<-" constr(T) :=
  trw_rev T || rewrite <- T.
Tactic Notation "rw" constr(T) "in" ident(H) :=
  trw_h T H || rewrite T in H.
Tactic Notation "rw" "<-" constr(T) "in" ident(H) :=
  trw_rev_h T H || rewrite <- T in H.

Tactic Notation "onerw" :=
       match goal with
         | [ H : _ |- _ ] ⇒ progress (trw H || rewrite H)
       end.

Tactic Notation "allrw" := repeat onerw.

Tactic Notation "allrw" "<-" :=
  repeat match goal with
           | [ H : _ |- _ ] ⇒ progress (trw_rev H || rewrite <- H)
          end.


Tactic Notation "onerw" constr(T) :=
       let t := type of T in
       match goal with
         | [ H : _, H' : t |- _ ] ⇒
             progress (trw_h T H || trw T || rewrite T in H || rewrite T)
         | [ H : t |- _ ] ⇒ fail 1
         | [ H : _ |- _ ] ⇒
             progress (trw_h T H || trw T || rewrite T in H || rewrite T)
       end.

Tactic Notation "allrw" constr(T) := repeat (onerw T).

Tactic Notation "rww" ident(T) :=
  let t := type of T in
  repeat match goal with
           | [ H1 : t, H : _ |- _ ] ⇒
             progress (trw_h T H || trw T || rewrite T in H || rewrite T)
         end.

Tactic Notation "allrw" "<-" constr(T) :=
  repeat match goal with
           | [ H : _ |- _ ] ⇒
             progress (trw_rev_h T H || trw_rev T || rewrite <- T in H || rewrite <- T)
         end.

Tactic Notation "rww" "<-" ident(T) :=
  let t := type of T in
  repeat match goal with
           | [ H1 : t, H : _ |- _ ] ⇒
             progress (trw_rev_h T H || trw_rev T || rewrite <- T in H || rewrite <- T)
         end.



setoid stuff -- delete?

Require Export Coq.Setoids.Setoid.

Inductive Cast (t : [univ]) : Prop :=
| cast : tCast t.
Hint Constructors Cast.

Inductive Cast2 (p : Prop) : [univ] :=
| cast2 : pCast2 p.
Hint Constructors Cast2.

Definition c_t_iff : relation [univ] :=
  fun A B : [univ]Cast (A <=> B).

Notation "x <==> y" := (c_t_iff x y) (at level 95, no associativity).

Definition t_c_iff : relation [univ] :=
  fun A B : [univ]Cast (AB) Cast (BA).

Notation "x <~> y" := (t_c_iff x y) (at level 95, no associativity).

Lemma CType_S : Setoid_Theory [univ] c_t_iff.
Proof.
  split.

  repeat constructor; auto.

  unfold Symmetric; intros.
  inversion H; subst.
  dall.
  repeat constructor; auto.

  unfold Transitive; intros.
  inversion H; inversion H0; subst.
  dall.
  repeat constructor; auto.
Qed.

Lemma TypeC_S : Setoid_Theory [univ] t_c_iff.
Proof.
  split.

  repeat constructor; auto.

  unfold Symmetric; intros.
  destruct H.
  inversion H; subst.
  inversion H0; subst.
  repeat constructor; auto.

  unfold Transitive; intros.
  destruct H; destruct H0.
  inversion H; inversion H0; inversion H1; inversion H2; subst.
  repeat constructor; auto.
Qed.

Add Setoid [univ] c_t_iff CType_S as Type_iff_reg.
Add Setoid [univ] t_c_iff TypeC_S as Type_iff_reg2.

Hint Resolve (Seq_refl [univ] c_t_iff CType_S): setoid.
Hint Resolve (Seq_sym [univ] c_t_iff CType_S): setoid.
Hint Resolve (Seq_trans [univ] c_t_iff CType_S): setoid.

Hint Resolve (Seq_refl [univ] t_c_iff TypeC_S): setoid.
Hint Resolve (Seq_sym [univ] t_c_iff TypeC_S): setoid.
Hint Resolve (Seq_trans [univ] t_c_iff TypeC_S): setoid.



should not be required anymore?

Tactic Notation "trewrite" "<-" ident(H) ident(p1) :=
  let name := fresh H in
  generalize (H p1);
    intro name;
    build_and_rewrite_rev name;
    clear name.

Tactic Notation "trewrite" "<-" ident(H) ident(p1) ident(p2) :=
  let name := fresh H in
  generalize (H p1 p2);
    intro name;
    build_and_rewrite_rev name;
    clear name.
Tactic Notation "trewrite" ident(H) ident(p1) :=
  let name := fresh H in
  generalize (H p1);
    intro name;
    build_and_rewrite name;
    clear name.

Tactic Notation "trewrite" ident(H) ident(p1) ident(p2) :=
  let name := fresh H in
  generalize (H p1 p2);
    intro name;
    build_and_rewrite name;
    clear name.

Tactic Notation "trewrite" ident(H) ident(p1) "in" ident (H') :=
  let name := fresh H in
  generalize (H p1);
    intro name;
    build_and_rewrite_hyp name H';
    clear name.

Tactic Notation "trewrite" ident(H) ident(p1) ident(p2) "in" ident (H') :=
  let name := fresh H in
  generalize (H p1 p2);
    intro name;
    build_and_rewrite_hyp name H';
    clear name.
Tactic Notation "trewrite" "<-" ident(H) ident(p1) "in" ident(H') :=
  let name := fresh H in
  generalize (H p1);
    intro name;
    build_and_rewrite_hyp_rev name H';
    clear name.

Tactic Notation "trewrite" "<-" ident(H) ident(p1) ident(p2) "in" ident(H') :=
  let name := fresh H in
  generalize (H p1 p2);
    intro name;
    build_and_rewrite_hyp_rev name H';
    clear name.

Theorem dont_touch_forall :
   (P Q : (nat : Set) → [univ]),
    ( (n : (nat : Set)), P n <=> ( (m : (nat : Set)), Q (m+n)))
    → P (1 : (nat : Set))
    → (m : (nat : Set)), Q (m+1).
Proof.
  intros ? ? Hif Hp1.

  rw Hif in Hp1; trivial.
Qed.

Theorem dont_touch_forall2 :
   (P Q : nat[univ]),
    ( n, P n <=> ( m, Q (m+n)))
    → P 1
    → m, Q (m+1).
Proof.
  intros ? ? Hif Hp1.
  trw_rev Hif. trivial.
Qed.

Theorem dont_touch_forall3 :
   (P Q: nat[univ]),
    ( n, P n <=> ( m, Q (m+n)))
    → ( m, Q (m+1))
    → P 1.
Proof.
  intros ? ? Hif Hq .
  trw_rev_h Hif Hq. trivial.
Qed.