Quelle bug_2164.v Sprache: Coq

(* Check that "inversion as" manages names as expected *)
Inductive type: Set
   := | int: type
      | pointer: type -> type.
Print type.

Parameter value_set
   : type -> Set.

Parameter string : Set.

Parameter Z : Set.

Inductive lvalue (t: type): Set
   := | var: string -> lvalue t (* name of the variable *)
      | lvalue_loc: Z -> lvalue t (* address of the variable *)
      | deref_l: lvalue (pointer t) -> lvalue t (* deref an lvalue ptr *)
      | deref_r: rvalue (pointer t) -> lvalue t (* deref an rvalue ptr *)
with rvalue (t: type): Set
   := | value_of: lvalue t -> rvalue t (* variable as value *)
      | mk_rvalue: value_set t -> rvalue t. (* literal value *)
Print lvalue.

Inductive statement: Set
   := | void_stat: statement
      | var_loc: (* to be destucted at end of scope *)
           forall (t: type) (n: string) (loc: Z), statement
      | var_ref: (* not to be destructed *)
           forall (t: type) (n: string) (loc: Z), statement
      | var_def: (* var def as typed in code *)
           forall (t:type) (n: string) (val: rvalue t), statement
      | assign:
           forall (t: type) (var: lvalue t) (val: rvalue t), statement
      | group:
           forall (l: list statement), statement
      | fun_def:
           forall (s: string) (l: list statement), statement
      | param_decl:
           forall (t: type) (n: string), statement
      | delete:
           forall a: Z, statement.

Inductive expr: Set
:= | statement_to_expr: statement -> expr
   | lvalue_to_expr: forall t: type, lvalue t -> expr
   | rvalue_to_expr: forall t: type, rvalue t -> expr.

Inductive executable_prim_expr: expr -> Set
:=
(* statements *)
   | var_def_primitive:
        forall (t: type) (n: string) (loc: Z),
        executable_prim_expr
           (statement_to_expr
               (var_def t n
                   (value_of t (lvalue_loc t loc))))
   | assign_primitive:
        forall (t: type) (loc1 loc2: Z),
        executable_prim_expr
           (statement_to_expr
               (assign t (lvalue_loc t loc1)
                   (value_of t (lvalue_loc t loc2))))
(* rvalue *)
   | mk_rvalue_primitive:
        forall (t: type) (v: value_set t),
        executable_prim_expr
           (rvalue_to_expr t (mk_rvalue t v))
(* lvalue *)
   (* var *)
   | var_primitive:
        forall (t: type) (n: string),
        executable_prim_expr (lvalue_to_expr t (var t n))
   (* deref_l *)
   | deref_l_primitive:
        forall (t: type) (loc: Z),
        executable_prim_expr
           (lvalue_to_expr t
               (deref_l t (lvalue_loc (pointer t) loc)))
   (* deref_r *)
   | deref_r_primitive:
        forall (t: type) (loc: Z),
        executable_prim_expr
           (lvalue_to_expr t
               (deref_r t
                   (value_of (pointer t)
                       (lvalue_loc (pointer t) loc)))).

Inductive executable_sub_expr: expr -> Set
:= | executable_sub_expr_prim:
        forall e: expr,
        executable_prim_expr e ->
        executable_sub_expr e
(* statements *)
   | var_def_sub_rvalue:
        forall (t: type) (n: string) (rv: rvalue t),
        executable_sub_expr (rvalue_to_expr t rv) ->
        executable_sub_expr (statement_to_expr (var_def t n rv))
   | assign_sub_lvalue:
        forall (t: type) (lv: lvalue t) (rv: rvalue t),
        executable_sub_expr (lvalue_to_expr t lv) ->
        executable_sub_expr (statement_to_expr (assign t lv rv))
   | assign_sub_rvalue:
        forall (t: type) (lv: lvalue t) (rv: rvalue t),
        executable_sub_expr (rvalue_to_expr t rv) ->
        executable_sub_expr (statement_to_expr (assign t lv rv))
(* rvalue *)
   | value_of_sub_lvalue:
        forall (t: type) (lv: lvalue t),
        executable_sub_expr (lvalue_to_expr t lv) ->
        executable_sub_expr (rvalue_to_expr t (value_of t lv))
(* lvalue *)
   | deref_l_sub_lvalue:
        forall (t: type) (lv: lvalue (pointer t)),
        executable_sub_expr (lvalue_to_expr (pointer t) lv) ->
        executable_sub_expr (lvalue_to_expr t (deref_l t lv))
   | deref_r_sub_rvalue:
        forall (t: type) (rv: rvalue (pointer t)),
        executable_sub_expr (rvalue_to_expr (pointer t) rv) ->
        executable_sub_expr (lvalue_to_expr t (deref_r t rv)).

Inductive expr_kind: Set
:= | statement_kind: expr_kind
   | lvalue_kind: type -> expr_kind
   | rvalue_kind: type -> expr_kind.

Definition expr_to_kind: expr -> expr_kind.
intro e.
destruct e.
exact statement_kind.
exact (lvalue_kind t).
exact (rvalue_kind t).
Defined.

Inductive def_sub_expr_subs:
   forall e: expr,
   forall ee: executable_sub_expr e,
   forall ee': expr,
   forall e': expr,
   Prop
:= | def_sub_expr_subs_prim:
        forall e: expr,
        forall p: executable_prim_expr e,
        forall ee': expr,
        expr_to_kind e = expr_to_kind ee' ->
        def_sub_expr_subs e (executable_sub_expr_prim e p) ee' ee'
   | def_sub_expr_subs_var_def_sub_rvalue:
        forall (t: type) (n: string),
        forall rv rv': rvalue t,
        forall ee': expr,
        forall se_rv: executable_sub_expr (rvalue_to_expr t rv),
        def_sub_expr_subs (rvalue_to_expr t rv) se_rv ee'
           (rvalue_to_expr t rv') ->
        def_sub_expr_subs
           (statement_to_expr (var_def t n rv))
           (var_def_sub_rvalue t n rv se_rv)
           ee'
           (statement_to_expr (var_def t n rv'))
   | def_sub_expr_subs_assign_sub_lvalue:
        forall t: type,
        forall lv lv': lvalue t,
        forall rv: rvalue t,
        forall ee': expr,
        forall se_lv: executable_sub_expr (lvalue_to_expr t lv),
        def_sub_expr_subs (lvalue_to_expr t lv) se_lv ee'
           (lvalue_to_expr t lv') ->
        def_sub_expr_subs
           (statement_to_expr (assign t lv rv))
           (assign_sub_lvalue t lv rv se_lv)
           ee'
           (statement_to_expr (assign t lv' rv))
   | def_sub_expr_subs_assign_sub_rvalue:
        forall t: type,
        forall lv: lvalue t,
        forall rv rv': rvalue t,
        forall ee': expr,
        forall se_rv: executable_sub_expr (rvalue_to_expr t rv),
        def_sub_expr_subs (rvalue_to_expr t rv) se_rv ee'
           (rvalue_to_expr t rv') ->
        def_sub_expr_subs
           (statement_to_expr (assign t lv rv))
           (assign_sub_rvalue t lv rv se_rv)
           ee'
           (statement_to_expr (assign t lv rv'))
   | def_sub_expr_subs_value_of_sub_lvalue:
        forall t: type,
        forall lv lv': lvalue t,
        forall ee': expr,
        forall se_lv: executable_sub_expr (lvalue_to_expr t lv),
        def_sub_expr_subs (lvalue_to_expr t lv) se_lv ee'
           (lvalue_to_expr t lv') ->
        def_sub_expr_subs
           (rvalue_to_expr t (value_of t lv))
           (value_of_sub_lvalue t lv se_lv)
           ee'
           (rvalue_to_expr t (value_of t lv'))
   | def_sub_expr_subs_deref_l_sub_lvalue:
        forall t: type,
        forall lv lv': lvalue (pointer t),
        forall ee': expr,
        forall se_lv: executable_sub_expr (lvalue_to_expr (pointer t) lv),
        def_sub_expr_subs (lvalue_to_expr (pointer t) lv) se_lv ee'
           (lvalue_to_expr (pointer t) lv') ->
        def_sub_expr_subs
           (lvalue_to_expr t (deref_l t lv))
           (deref_l_sub_lvalue t lv se_lv)
           ee'
           (lvalue_to_expr t (deref_l t lv'))
   | def_sub_expr_subs_deref_r_sub_rvalue:
        forall t: type,
        forall rv rv': rvalue (pointer t),
        forall ee': expr,
        forall se_rv: executable_sub_expr (rvalue_to_expr (pointer t) rv),
        def_sub_expr_subs (rvalue_to_expr (pointer t) rv) se_rv ee'
           (rvalue_to_expr (pointer t) rv') ->
        def_sub_expr_subs
           (lvalue_to_expr t (deref_r t rv))
           (deref_r_sub_rvalue t rv se_rv)
           ee'
           (lvalue_to_expr t (deref_r t rv')).

Lemma type_dec: forall t t': type, {t = t'} + {t <> t'}.
Proof.
intros t.
induction t as [|t IH].
destruct t'.
tauto.
right.
discriminate.
destruct t'.
right.
discriminate.
destruct (IH t') as [H|H].
left.
f_equal.
tauto.
right.
injection.
tauto.
Qed.
Check type_dec.

Definition sigT_get_proof:
   forall T: Type,
   forall eq_dec_T: forall t t': T, {t = t'} + {~ t = t'},
   forall P: T -> Type,
   forall t: T,
   P t ->
   sigT P ->
      P t.
intros T eq_dec_T P t H1 H2.
destruct H2 as [t' H2].
destruct (eq_dec_T t t') as [H3|H3].
rewrite H3.
exact H2.
exact H1.
Defined.

Axiom sigT_get_proof_existT_same:
   forall T: Type,
   forall eq_dec_T: forall t t': T, {t = t'} + {~ t = t'},
   forall P: T -> Type,
   forall t: T,
   forall H1 H2: P t,
   sigT_get_proof T eq_dec_T P t H1 (existT P t H2) = H2.

Theorem existT_injective:
   forall T,
   (forall t1 t2: T, { t1 = t2 } + { t1 <> t2 }) ->
   forall P: T -> Type,
   forall t: T,
   forall pt1 pt2: P t,
   existT P t pt1 = existT P t pt2 ->
   pt1 = pt2.
Proof.
intros T T_dec P t pt1 pt2 H1.
pose (H2 := f_equal (sigT_get_proof T T_dec P t pt1) H1).
repeat rewrite sigT_get_proof_existT_same in H2.
assumption.
Qed.

Ltac decide_equality_sub dec x x' H :=
   destruct (dec x x') as [H|H];
   [subst x'; try tauto|try(right; injection; tauto; fail)].

Axiom value_set_dec:
   forall t: type,
   forall v v': value_set t,
      {v = v'} + {v <> v'}.

Theorem lvalue_dec:
   forall (t: type) (l l': lvalue t), {l = l'} + {l <> l'}
with rvalue_dec:
   forall (t: type) (r r': rvalue t), {r = r'} + {r <> r'}.
Admitted.

Theorem sub_expr_subs_same_kind:
   forall e: expr,
   forall ee: executable_sub_expr e,
   forall ee': expr,
   forall e': expr,
   def_sub_expr_subs e ee ee' e' ->
   expr_to_kind e = expr_to_kind e'.
Proof.
intros e ee ee' e' H1.
case H1; try (intros; tauto; fail).
Qed.

Theorem def_sub_expr_subs_assign_sub_lvalue_inversion:
   forall t: type,
   forall lv: lvalue t,
   forall rv: rvalue t,
   forall ee' e': expr,
   forall ee_sub: executable_sub_expr (lvalue_to_expr t lv),
   def_sub_expr_subs (statement_to_expr (assign t lv rv))
      (assign_sub_lvalue t lv rv ee_sub) ee' e' ->
   { lv': lvalue t
   | def_sub_expr_subs (lvalue_to_expr t lv) ee_sub ee'
        (lvalue_to_expr t lv')
   & e' = statement_to_expr (assign t lv' rv) }.
Proof.
intros t lv rv ee' [s'|t' lv''|t' rv''] ee_sub H1;
   try discriminate (sub_expr_subs_same_kind _ _ _ _ H1).
destruct s' as [| | | |t' lv'' rv''| | | |];
   try(assert (H2: False); [inversion H1|elim H2]; fail).
destruct (type_dec t t') as [H2|H2];
   [|assert (H3: False);
     [|elim H3; fail]].
2: inversion H1 as [];tauto.
subst t'.
exists lv''.
inversion H1 as
   [| |t' lv''' lv'''' rv''' ee'' ee_sub' H2 (H3_1,H3_2,H3_3) (H4_1,H4_2,H4_3,H4_4,H4_5) H5 (H6_1,H6_2)| | | |].
(* Check that all names are the given ones: *)
clear t' lv''' lv'''' rv''' ee'' ee_sub' H2 H3_1 H3_2 H3_3 H4_1 H4_2 H4_3 H4_4 H4_5 H5 H6_1 H6_2.
Abort.

quality99%

¤ Dauer der Verarbeitung: 0.12 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.