Quelle congruence.v Sprache: Coq

Inductive Inner : Type :=
| innerI_nat : forall (x:nat), Inner
| innerI_fun : forall (f:nat->Type), Inner
| innerI_inner : forall (i:Inner), Inner
| innerI_Type : forall (T:Type), Inner
| innerI_extra : Inner.

Inductive ExtractTest (A:Type) (F:nat->Type) (I:Inner): Inner -> Inner -> unit -> Type :=
| extract_f_x_from_index : forall (x:nat) (f:nat->Type) (t:f x),
    ExtractTest A F I (innerI_inner (innerI_nat x)) (innerI_fun f) tt
| extract_F_from_param_x_from_index : forall (x:nat) (f:nat->Type) (t:F x),
    ExtractTest A F I (innerI_inner (innerI_nat x)) innerI_extra tt
| extract_fail : forall (x y: nat) (f : nat -> Type) (t : f x),
    ExtractTest A F I (innerI_nat y) (innerI_fun f) tt
| extract_fx_from_index : forall (x:nat) (f:nat->Type) (t:f x),
    ExtractTest A F I (innerI_Type (f x)) innerI_extra tt
| extract_t_match : forall (b:bool) (t:if b then unit else nat),
    ExtractTest A F I (innerI_Type (if b then unit else nat)) innerI_extra tt
.

(* This still dosn't work, because the fields type isn't composeable from extracteable parts of its inductive type.*)
Lemma test_extract_fail A F x y f t1 t2 : extract_fail A F innerI_extra x y f t1 = extract_fail A F innerI_extra x y f t2 -> t1 = t2.
Proof.
    Fail congruence.
Abort.

(* I think this should also work when the whole match statement is part of the inductive type, but something with universes is wrong because A is Type but if b then unit else nat is Set below is the projection that is getting created but it doesn't work *)
Lemma test_extract_t_match_success (A:Set) (F:nat->Type) (b:bool) (t1 t2: if b then unit else nat) :
extract_t_match A F innerI_extra b t1 = extract_t_match A F innerI_extra b t2 -> t1 = t2.
Proof.
    intros H.
    Fail congruence.
Abort.

Fail Definition proj (A:Type) (F:nat->Type) (b:bool) (t1:if b then unit else nat):=
    (fun
    e : ExtractTest A F innerI_extra
          (innerI_Type (if b then unit else nat)) innerI_extra tt =>
  match
    e in (ExtractTest _ _ _ i i0 u)
    return
      (match i with
       | innerI_Type T => T
       | _ => if b then unit else nat
       end ->
       match i with
       | innerI_Type T => T
       | _ => if b then unit else nat
       end)
  with
  | extract_f_x_from_index _ _ _ x f _ =>
      fun
        t : match innerI_inner (innerI_nat x) with
            | innerI_Type T => T
            | _ => if b then unit else nat
            end =>
      t
  | extract_F_from_param_x_from_index _ _ _ x _ _ =>
      fun
        t : match innerI_inner (innerI_nat x) with
            | innerI_Type T => T
            | _ => if b then unit else nat
            end =>
      t
  | extract_fail _ _ _ x y f _ =>
      fun
        t : match innerI_nat y with
            | innerI_Type T => T
            | _ => if b then unit else nat
            end =>
      t
  | extract_fx_from_index _ _ _ x f _ =>
      fun
        t : match innerI_Type (f x) with
            | innerI_Type T => T
            | _ => if b then unit else nat
            end =>
      t
  | extract_t_match _ _ _ b0 t =>
      fun
        _ : match innerI_Type (if b0 then unit else nat) with
            | innerI_Type T => T
            | _ => if b then unit else nat
            end =>
      t
  end t1).

quality99%

¤ Dauer der Verarbeitung: 0.4 Sekunden ¤

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.