Library eq_rel
Require Export universe.
Inductive void : [univ] := .
Inductive t_iff (A B : [univ]) : [univ] :=
| t_iff_cons : (A → B) → (B → A) → 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) <=> ((A → B) # (B → A)).
Proof.
intros; split; intros k; split; intros; destruct k; auto.
Qed.
Lemma tiff_is_prod_implies2 :
∀ A B : [univ],
((A → B) # (B → A)) <=> (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') → ((A → B) <=> (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
| a ⇒ p
| ?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 → ?H ⇒ fail 1
| ?H → ?H2 ⇒
clear name;
assert (H <=> H2) as Hn by (apply T)
end
| ?Hl <=> ?Hr ⇒ get_instance_of T Hl Hn || get_instance_of T Hr Hn
| ?Hl # ?Hr ⇒ get_instance_of T Hl Hn || get_instance_of T Hr Hn
| ?Hl [+] ?Hr ⇒ get_instance_of T Hl Hn || get_instance_of T Hr Hn
| !?Hl ⇒ get_instance_of T Hl Hn
| ?Hl → ?Hr ⇒ get_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 → ?H ⇒ fail 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 <=> ?Hr ⇒ get_instance_of_rev T Hl Hn || get_instance_of_rev T Hr Hn
| ?Hl # ?Hr ⇒ get_instance_of_rev T Hl Hn || get_instance_of_rev T Hr Hn
| ?Hl [+] ?Hr ⇒ get_instance_of_rev T Hl Hn || get_instance_of_rev T Hr Hn
| !?Hl ⇒ get_instance_of_rev T Hl Hn
| ?Hl → ?Hr ⇒ get_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.
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 : t → Cast t.
Hint Constructors Cast.
Inductive Cast2 (p : Prop) : [univ] :=
| cast2 : p → Cast2 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 (A → B) ∧ Cast (B → A).
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.