Quelle InversionSigma.v Sprache: Coq

Section inversion_sigma.
  Local Unset Implicit Arguments.
  Context A (B B' : A -> Prop) (C C' : forall a, B a -> Prop)
          (D : forall a b, C a b -> Prop) (E : forall a b c, D a b c -> Prop).
  Context (AP : Prop) (BP BP' : AP -> Prop) (CP CP' : forall a, BP a -> Prop)
          (DP : forall a b, CP a b -> Prop) (EP : forall a b c, DP a b c -> Prop).

  (* Require that, after destructing sigma types and inverting
     equalities, we can subst equalities of variables only, and reduce
     down to [eq_refl = eq_refl]. *)
  Local Ltac destr_sigma :=
    repeat match goal with
           | [ H : ex _ |- _ ] => destruct H
           | [ H : sig _ |- _ ] => destruct H
           | [ H : sigT _ |- _ ] => destruct H
           | [ H : ex2 _ _ |- _ ] => destruct H
           | [ H : sig2 _ _ |- _ ] => destruct H
           | [ H : sigT2 _ _ |- _ ] => destruct H
           end; simpl in *.
  Local Ltac fin_test_inversion_sigma :=
    match goal with
    | [ |- eq_refl = eq_refl ] => reflexivity
    end.
  Local Ltac test_inversion_sigma :=
    intros;
    destr_sigma;
    inversion_sigma;
    repeat match goal with
           | [ H : ?x = ?y |- _ ] => is_var x; is_var y; subst x; simpl in *
           end;
    fin_test_inversion_sigma.

  Local Ltac test_inversion_sigma_in_H :=
    intros;
    destr_sigma;
    repeat match goal with H : _ = _ |- _ => inversion_sigma H end;
    repeat match goal with
           | [ H : ?x = ?y |- _ ] => is_var x; is_var y; subst x; simpl in *
           end;
    fin_test_inversion_sigma.

  Goal forall (x y : { a : A & { b : { b : B a & C a b } & { d : D a (projT1 b) (projT2 b) & E _ _ _ d } } })
              (p : x = y), p = p.
  Proof.
    intros x y p; destr_sigma.
    inversion_sigma p as [-> p]; cbn [eq_rect] in *.
    lazymatch type of p with
    | existT _ (existT _ ?a ?b) (existT _ ?c ?d) = existT _ (existT _ ?e ?f) (existT _ ?g ?h)
      => is_var a; is_var b; is_var c; is_var d; is_var e; is_var f; is_var g; is_var h
    end.
    inversion_sigma p as [p1 p2].
    lazymatch type of p1 with existT _ ?a ?b = existT _ ?c ?d => is_var a; is_var b; is_var c; is_var d end.
    inversion_sigma p1 as [-> <-]; cbn [eq_rect eq_existT_uncurried eq_sigT eq_existT_curried eq_sigT_uncurried] in * |- .
    lazymatch type of p2 with existT _ ?a ?b = existT _ ?c ?d => is_var a; is_var b; is_var c; is_var d end.
    inversion_sigma p2 as [-> <-].
    cbn.
    fin_test_inversion_sigma.
  Qed.

  Goal forall (x y : { a : A | { b : { b : B a | C a b } | { d : D a (proj1_sig b) (proj2_sig b) | E _ _ _ d } } })
              (p : x = y), p = p.
  Proof.
    intros x y p; destr_sigma.
    inversion_sigma p as [-> p]; cbn [eq_rect] in *.
    lazymatch type of p with
    | exist _ (exist _ ?a ?b) (exist _ ?c ?d) = exist _ (exist _ ?e ?f) (exist _ ?g ?h)
      => is_var a; is_var b; is_var c; is_var d; is_var e; is_var f; is_var g; is_var h
    end.
    inversion_sigma p as [p1 p2].
    lazymatch type of p1 with exist _ ?a ?b = exist _ ?c ?d => is_var a; is_var b; is_var c; is_var d end.
    inversion_sigma p1 as [-> <-]; cbn [eq_rect eq_exist_uncurried eq_sig eq_exist_curried eq_sig_uncurried] in * |- .
    lazymatch type of p2 with exist _ ?a ?b = exist _ ?c ?d => is_var a; is_var b; is_var c; is_var d end.
    inversion_sigma p2 as [-> <-].
    cbn.
    fin_test_inversion_sigma.
  Qed.

  Goal forall (x y : exists a : AP, exists b : exists b : BP a, CP a b, exists d : DP a (ex_proj1 b) (ex_proj2 b), EP _ _ _ d)
              (p : x = y), p = p.
  Proof.
    intros x y p; destr_sigma.
    inversion_sigma p as [-> p]; cbn [eq_rect] in *.
    lazymatch type of p with
    | ex_intro _ (ex_intro _ ?a ?b) (ex_intro _ ?c ?d) = ex_intro _ (ex_intro _ ?e ?f) (ex_intro _ ?g ?h)
      => is_var a; is_var b; is_var c; is_var d; is_var e; is_var f; is_var g; is_var h
    end.
    inversion_sigma p as [p1 p2].
    lazymatch type of p1 with ex_intro _ ?a ?b = ex_intro _ ?c ?d => is_var a; is_var b; is_var c; is_var d end.
    inversion_sigma p1 as [-> <-]; cbn [eq_rect eq_ex_intro_uncurried eq_ex_intro eq_ex eq_ex_uncurried] in * |- .
    lazymatch type of p2 with ex_intro _ ?a ?b = ex_intro _ ?c ?d => is_var a; is_var b; is_var c; is_var d end.
    inversion_sigma p2 as [-> <-].
    cbn.
    fin_test_inversion_sigma.
  Qed.

  Goal forall (x y : { a : { a : A & B a } & C _ (projT2 a) & C' _ (projT2 a) })
              (p : x = y), p = p.
  Proof.
    intros x y p; destr_sigma.
    inversion_sigma p as [p <- <-]; cbn [eq_rect] in *.
    lazymatch type of p with existT _ ?a ?b = existT _ ?c ?d => is_var a; is_var b; is_var c; is_var d end.
    inversion_sigma p as [-> <-].
    cbn.
    fin_test_inversion_sigma.
  Qed.

  Goal forall (x y : { a : { a : A & B a } | C _ (projT2 a) & C' _ (projT2 a) })
              (p : x = y), p = p.
  Proof.
    intros x y p; destr_sigma.
    inversion_sigma p as [p <- <-]; cbn [eq_rect] in *.
    lazymatch type of p with existT _ ?a ?b = existT _ ?c ?d => is_var a; is_var b; is_var c; is_var d end.
    inversion_sigma p as [-> <-].
    cbn.
    fin_test_inversion_sigma.
  Qed.

  Goal forall (x y : exists2 a : exists a : AP, BP a, CP _ (ex_proj2 a) & CP' _ (ex_proj2 a))
              (p : x = y), p = p.
  Proof.
    intros x y p; destr_sigma.
    inversion_sigma p as [p <- <-]; cbn [eq_rect] in *.
    lazymatch type of p with ex_intro _ ?a ?b = ex_intro _ ?c ?d => is_var a; is_var b; is_var c; is_var d end.
    inversion_sigma p as [-> <-].
    cbn.
    fin_test_inversion_sigma.
  Qed.

  Goal forall (x y : { a : { a : A & B a & B' a } & C _ (projT2 (sigT_of_sigT2 a)) & C' _ (projT2 (sigT_of_sigT2 a)) })
              (p : x = y), p = p.
  Proof.
    intros x y p; destr_sigma.
    inversion_sigma p as [p <- <-]; cbn [eq_rect] in *.
    lazymatch type of p with existT2 _ _ ?a ?b ?c = existT2 _ _ ?d ?e ?f => is_var a; is_var b; is_var c; is_var d; is_var e; is_var f end.
    inversion_sigma p as [-> <- <-].
    cbn.
    fin_test_inversion_sigma.
  Qed.

  Goal forall (x y : { a : { a : A & B a & B' a } | C _ (projT2 (sigT_of_sigT2 a)) & C' _ (projT2 (sigT_of_sigT2 a)) })
              (p : x = y), p = p.
  Proof.
    intros x y p; destr_sigma.
    inversion_sigma p as [p <- <-]; cbn [eq_rect] in *.
    lazymatch type of p with existT2 _ _ ?a ?b ?c = existT2 _ _ ?d ?e ?f => is_var a; is_var b; is_var c; is_var d; is_var e; is_var f end.
    inversion_sigma p as [-> <- <-].
    cbn.
    fin_test_inversion_sigma.
  Qed.

  Goal forall (x y : exists2 a : exists2 a : AP, BP a & BP' a, CP _ (ex_proj2 (ex_of_ex2 a)) & CP' _ (ex_proj2 (ex_of_ex2 a)))
              (p : x = y), p = p.
  Proof.
    intros x y p; destr_sigma.
    inversion_sigma p as [p <- <-]; cbn [eq_rect] in *.
    lazymatch type of p with ex_intro2 _ _ ?a ?b ?c = ex_intro2 _ _ ?d ?e ?f => is_var a; is_var b; is_var c; is_var d; is_var e; is_var f end.
    inversion_sigma p as [-> <- <-].
    cbn.
    fin_test_inversion_sigma.
  Qed.

  Goal forall (x y : { a : A & { b : { b : B a & C a b } & { d : D a (projT1 b) (projT2 b) & E _ _ _ d } } })
              (p : x = y), p = p.
  Proof. test_inversion_sigma. Qed.

  Goal forall (x y : { a : A | { b : { b : B a | C a b } | { d : D a (proj1_sig b) (proj2_sig b) | E _ _ _ d } } })
              (p : x = y), p = p.
  Proof. test_inversion_sigma. Qed.

  Goal forall (x y : exists a : AP, exists b : exists b : BP a, CP a b, exists d : DP a (ex_proj1 b) (ex_proj2 b), EP _ _ _ d)
              (p : x = y), p = p.
  Proof. test_inversion_sigma. Qed.

  Goal forall (x y : { a : { a : A & B a } & C _ (projT2 a) & C' _ (projT2 a) })
              (p : x = y), p = p.
  Proof. test_inversion_sigma. Qed.

  Goal forall (x y : { a : { a : A & B a } | C _ (projT2 a) & C' _ (projT2 a) })
              (p : x = y), p = p.
  Proof. test_inversion_sigma. Qed.

  Goal forall (x y : { a : { a : A & B a & B' a } | C _ (projT2 (sigT_of_sigT2 a)) & C' _ (projT2 (sigT_of_sigT2 a)) })
              (p : x = y), p = p.
  Proof. test_inversion_sigma. Qed.

  Goal forall (x y : { a : { a : A & B a & B' a } | C _ (projT2 (sigT_of_sigT2 a)) & C' _ (projT2 (sigT_of_sigT2 a)) })
              (p : x = y), p = p.
  Proof. test_inversion_sigma. Qed.

  Goal forall (x y : exists2 a : exists2 a : AP, BP a & BP' a, CP _ (ex_proj2 (ex_of_ex2 a)) & CP' _ (ex_proj2 (ex_of_ex2 a)))
              (p : x = y), p = p.
  Proof. test_inversion_sigma. Qed.

  Goal forall (x y : { a : A & { b : { b : B a & C a b } & { d : D a (projT1 b) (projT2 b) & E _ _ _ d } } })
              (p : x = y), p = p.
  Proof. test_inversion_sigma_in_H. Qed.

  Goal forall (x y : { a : A | { b : { b : B a | C a b } | { d : D a (proj1_sig b) (proj2_sig b) | E _ _ _ d } } })
              (p : x = y), p = p.
  Proof. test_inversion_sigma_in_H. Qed.

  Goal forall (x y : exists a : AP, exists b : exists b : BP a, CP a b, exists d : DP a (ex_proj1 b) (ex_proj2 b), EP _ _ _ d)
              (p : x = y), p = p.
  Proof. test_inversion_sigma_in_H. Qed.

  Goal forall (x y : { a : { a : A & B a } & C _ (projT2 a) & C' _ (projT2 a) })
              (p : x = y), p = p.
  Proof. test_inversion_sigma_in_H. Qed.

  Goal forall (x y : { a : { a : A & B a } | C _ (projT2 a) & C' _ (projT2 a) })
              (p : x = y), p = p.
  Proof. test_inversion_sigma_in_H. Qed.

  Goal forall (x y : { a : { a : A & B a & B' a } | C _ (projT2 (sigT_of_sigT2 a)) & C' _ (projT2 (sigT_of_sigT2 a)) })
              (p : x = y), p = p.
  Proof. test_inversion_sigma_in_H. Qed.

  Goal forall (x y : { a : { a : A & B a & B' a } | C _ (projT2 (sigT_of_sigT2 a)) & C' _ (projT2 (sigT_of_sigT2 a)) })
              (p : x = y), p = p.
  Proof. test_inversion_sigma_in_H. Qed.

  Goal forall (x y : exists2 a : exists2 a : AP, BP a & BP' a, CP _ (ex_proj2 (ex_of_ex2 a)) & CP' _ (ex_proj2 (ex_of_ex2 a)))
              (p : x = y), p = p.
  Proof. test_inversion_sigma_in_H. Qed.
End inversion_sigma.

quality99%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.