diff options
Diffstat (limited to 'test-suite/bugs/closed/2164.v')
| -rw-r--r-- | test-suite/bugs/closed/2164.v | 334 |
1 files changed, 334 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2164.v b/test-suite/bugs/closed/2164.v new file mode 100644 index 00000000..6adb3577 --- /dev/null +++ b/test-suite/bugs/closed/2164.v @@ -0,0 +1,334 @@ +(* 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. |