Coq source for verifying example cases for voidness preservation criteria

test.v

Require Import List.
Require Import voidness.

(* ---------- Dart types ---------- *)

(* Object *)
Definition ct_Object : ClassTypes := (Object, nil) :: nil.
Definition dt_Object := dt_class ct_Object.

(* A<Object> *)
Definition ct_A_Object := (A, dt_Object :: nil) :: ct_Object.
Definition dt_A_Object := dt_class ct_A_Object.

(* A<void> *)
Definition ct_A_void := (A, dt_void :: nil) :: ct_Object.
Definition dt_A_void := dt_class ct_A_void.

(* A<dynamic> *)
Definition ct_A_dynamic := (A, dt_dynamic :: nil) :: ct_Object.
Definition dt_A_dynamic := dt_class ct_A_dynamic.

(* Iterable<Object> *)
Definition ct_Iterable_Object := (Iterable, dt_Object :: nil) :: ct_Object.
Definition dt_Iterable_Object := dt_class ct_Iterable_Object.

(* Iterable<void> *)
Definition ct_Iterable_void := (Iterable, dt_void :: nil) :: ct_Object.
Definition dt_Iterable_void := dt_class ct_Iterable_void.

(* List<Object> *)
Definition ct_List_Object := (List, dt_Object :: nil) :: ct_Iterable_Object.
Definition dt_List_Object := dt_class ct_List_Object.

(* List<void> *)
Definition ct_List_void := (List, dt_void :: nil) :: ct_Iterable_void.
Definition dt_List_void := dt_class ct_List_void.

Definition dt_fun_void_void := dt_function dt_void (dt_void :: nil).
Definition dt_fun_void_dynamic := dt_function dt_dynamic (dt_void :: nil).
Definition dt_fun_dynamic_void := dt_function dt_void (dt_dynamic :: nil).
Definition dt_fun_dynamic_dynamic := dt_function dt_dynamic (dt_dynamic :: nil).
Definition dt_fun_Object_Object := dt_function dt_Object (dt_Object :: nil).
Definition dt_fun_Object_void := dt_function dt_void (dt_Object :: nil).
Definition dt_fun_void_Object := dt_function dt_Object (dt_void :: nil).

(* ---------- Voidness Types ---------- *)

(* Object *)
Definition cvt_Object : VoidnessClassTypes := (Object, nil) :: nil.
Definition vt_Object := vt_class cvt_Object.

(* A<Object> *)
Definition cvt_A_Object := (A, vt_Object :: nil) :: cvt_Object.
Definition vt_A_Object := vt_class cvt_A_Object.

(* A<1> *)
Definition cvt_A_1 := (A, vt_1 :: nil) :: cvt_Object.
Definition vt_A_1 := vt_class cvt_A_1.

(* A<A<1>> *)
Definition cvt_A_A_1 := (A, vt_A_1 :: nil) :: cvt_Object.
Definition vt_A_A_1 := vt_class cvt_A_A_1.

(* Object Function() *)
Definition vt_fun_Object_nil := vt_function vt_Object nil.

(* A<1> Function(A<A<1>>) *)
Definition vt_fun_A1_AA1 := vt_function vt_A_1 (vt_A_A_1 :: nil).

(* B<A<1>, Object> *)
Definition cvt_B_A1_Object := (B, vt_A_1 :: vt_Object :: nil) :: cvt_Object.
Definition vt_B_A1_Object := vt_class cvt_B_A1_Object.

(* B<Object, Object> *)
Definition cvt_B_ObjectObject := (B, vt_Object :: vt_Object :: nil) :: cvt_Object.
Definition vt_B_ObjectObject := vt_class cvt_B_ObjectObject.

Hint Unfold
  ct_Object dt_Object ct_A_Object dt_A_Object ct_A_void dt_A_void
  ct_A_dynamic dt_A_dynamic ct_Iterable_Object dt_Iterable_Object
  ct_Iterable_void dt_Iterable_void ct_List_Object dt_List_Object
  ct_List_void dt_List_void dt_fun_void_void dt_fun_void_dynamic
  dt_fun_dynamic_void dt_fun_dynamic_dynamic dt_fun_Object_Object
  dt_fun_Object_void dt_fun_void_Object cvt_Object vt_Object
  cvt_A_Object vt_A_Object cvt_A_1 vt_A_1 cvt_A_A_1 vt_A_A_1
  vt_fun_Object_nil vt_fun_A1_AA1 cvt_B_A1_Object vt_B_A1_Object
  cvt_B_ObjectObject vt_B_ObjectObject.

(* ---------- Trying out existing examples ---------- *)

(* 0 <:: 0 *)
Goal VoidnessPreserves vt_0 vt_0.
 auto.
Qed.

(* 0 <:: 1 *)
Goal VoidnessPreserves vt_0 vt_1.
  auto.
Qed.

(* A<Object> <:: A<1> *)
Lemma L1 : VoidnessPreserves vt_A_Object vt_A_1.
Proof.
  apply vp_class; apply vctsp_cons.
    apply vctp_some; apply vctps_first; auto.
  apply vctsp_cons; auto.
  apply vctp_some. apply vctps_rest. apply vctps_first. auto.
Qed.

(* A<A<1>> <:: A<1> *)
Lemma L2 : VoidnessPreserves vt_A_A_1 vt_A_1.
Proof.
  apply vp_class; apply vctsp_cons; auto.
    apply vctp_some. apply vctps_first. apply vpp_cons; auto.
  apply vctsp_cons; auto. apply vctp_some. apply vctps_rest. apply vctps_first. auto.
Qed.

Lemma L3 : ~(VoidnessPreserves vt_A_1 vt_A_Object).
Proof.
  unfold not. intro H. inversion H. inversion H2. inversion H5.
    inversion H8. apply H14. reflexivity.
  inversion H8.
    inversion H12. inversion H19.
  inversion H13. inversion H17. 
Qed.
  
(* -------------------- Examples from email threads -------------------- *)

(* A<Object> x = new A<void>(); // No *)
Lemma L4 : ~(TypeVoidnessPreserves dt_A_void dt_A_Object).
Proof.
  unfold not. intro H. inversion H. inversion H2. inversion H5.
    inversion H8. apply H14. reflexivity.
  inversion H8.
    inversion H12. inversion H19.
  inversion H13. inversion H17. 
Qed.

(* A<dynamic> x = new A<void>(); // Yes *)
Lemma L5 : TypeVoidnessPreserves dt_A_void dt_A_dynamic.
Proof.
  unfold TypeVoidnessPreserves. simpl. auto 7.
Qed.

(* A<Object> x = new A<dynamic>(); // Yes *)
Lemma L6 : TypeVoidnessPreserves dt_A_void dt_A_dynamic.
Proof.
  unfold TypeVoidnessPreserves. simpl. auto 7.
Qed.

(* A<void> x = new A<dynamic>(); // voidV = dynamicV, yes *)
Lemma L7 : TypeVoidnessPreserves dt_A_dynamic dt_A_void.
Proof.
  unfold TypeVoidnessPreserves. simpl. auto 7.
Qed.

(* A<void> x = new A<Object>(); // voidV = objectV, Yes *)
Lemma L8 : TypeVoidnessPreserves dt_A_Object dt_A_void.
Proof.
  unfold TypeVoidnessPreserves. simpl. auto 7.
Qed.

(* dynamic x = new A<void>(); // Yes *)
Lemma L9 : TypeVoidnessPreserves dt_A_void dt_dynamic.
Proof.
  unfold TypeVoidnessPreserves. simpl. auto 7.
Qed.

(* Object x = new A<void>(); // Yes *)
Lemma L10 : TypeVoidnessPreserves dt_A_void dt_Object.
Proof.
  unfold TypeVoidnessPreserves. simpl.
  apply vp_class. apply vctsp_cons.
    apply vctp_gone. apply vctg_cons.
      discriminate.
    apply vctg_nil.
  apply vctsp_cons.
    apply vctp_some. auto.
  auto.
Qed.

(* Iterable<void> x = new List<void>(); // Yes *)
Lemma L11 : TypeVoidnessPreserves dt_List_void dt_Iterable_void.
Proof.
  unfold TypeVoidnessPreserves. simpl.
  apply vp_class. apply vctsp_cons.
    apply vctp_gone; apply vctg_cons.
      discriminate.
    apply vctg_cons.
      discriminate.
    auto.
  apply vctsp_cons.
    apply vctp_some. apply vctps_first. auto.
  apply vctsp_cons.
    apply vctp_some. apply vctps_rest. apply vctps_first. auto.
  auto.
Qed.

(* List<void> x = new Iterable<void>(); // Yes *)
Lemma L12 : TypeVoidnessPreserves dt_Iterable_void dt_List_void.
Proof.
  unfold TypeVoidnessPreserves. simpl. auto 8.
Qed.

(* Iterable<Object> x = new List<void>(); // No *)
Lemma L13 : ~(TypeVoidnessPreserves dt_List_void dt_Iterable_Object).
Proof.
  unfold TypeVoidnessPreserves.
  simpl. unfold not. intros. inversion H.
  inversion H2. inversion H7. inversion H10.
    inversion H13. apply H19. reflexivity.
  inversion H13.
    inversion H17. inversion H24.
  inversion H18. inversion H22.
Qed.

(* List<Object> x = new Iterable<void>(); // No *)
Lemma L14 : ~(TypeVoidnessPreserves dt_Iterable_void dt_List_Object).
Proof.
  unfold TypeVoidnessPreserves.
  simpl. unfold not. intros. inversion H.
  inversion H2. inversion H5.
    inversion H8. inversion H17. apply H21. reflexivity.
  inversion H8. inversion H13.
    inversion H16. inversion H23.
  inversion H17. inversion H21.
Qed.

(* void Function(void) f = func<dynamic, dynamic>; // Yes!! void-to-dynamic is OK! *)
Lemma L15 : TypeVoidnessPreserves dt_fun_dynamic_dynamic dt_fun_void_void.
Proof.
  unfold TypeVoidnessPreserves. simpl. auto.
Qed.

(* void Function(void) f = func<dynamic, void>; // Yes!! void-to-dynamic is OK! *)
Lemma L16 : TypeVoidnessPreserves dt_fun_dynamic_void dt_fun_void_void.
Proof.
  unfold TypeVoidnessPreserves.
  simpl. auto.
Qed.

(* void Function(void) f = func<void, dynamic>; // Yes *)
Lemma L17 : TypeVoidnessPreserves dt_fun_void_dynamic dt_fun_void_void.
Proof.
  unfold TypeVoidnessPreserves.
  simpl. auto.
Qed.

(* void Function(void) f = func<Object, Object>; // No *)
Lemma L18 : ~(TypeVoidnessPreserves dt_fun_Object_Object dt_fun_void_void).
Proof.
  unfold TypeVoidnessPreserves.
  simpl. unfold not. intros. inversion H. inversion H5. inversion H9.
Qed.

(* void Function(void) f = func<Object, void>; // No *)
Lemma L19 : ~(TypeVoidnessPreserves dt_fun_Object_void dt_fun_void_void).
Proof.
  unfold TypeVoidnessPreserves.
  simpl. unfold not. intros. inversion H. inversion H5. inversion H9.
Qed.

(* void Function(void) f = func<void, Object>; // Yes *)
Lemma L20 : TypeVoidnessPreserves dt_fun_void_Object dt_fun_void_void.
Proof.
  unfold TypeVoidnessPreserves.
  simpl. auto.
Qed.

(* dynamic Function(dynamic) g = func<void, void>; // Yes *)
Lemma L21 : TypeVoidnessPreserves dt_fun_void_void dt_fun_dynamic_dynamic.
Proof.
  unfold TypeVoidnessPreserves.
  simpl. auto.
Qed.

(* dynamic Function(dynamic) g = func<dynamic, void>; // Yes *)
Lemma L22 : TypeVoidnessPreserves dt_fun_dynamic_void dt_fun_dynamic_dynamic.
Proof.
  unfold TypeVoidnessPreserves.
  simpl. auto.
Qed.

(* dynamic Function(dynamic) g = func<void, dynamic>; // Yes *)
Lemma L23 : TypeVoidnessPreserves dt_fun_void_dynamic dt_fun_dynamic_dynamic.
Proof.
  unfold TypeVoidnessPreserves.
  simpl. auto.
Qed.

(* dynamic Function(dynamic) g = func<Object, Object>; // Yes *)
Lemma L24 : TypeVoidnessPreserves dt_fun_Object_Object dt_fun_dynamic_dynamic.
Proof.
  unfold TypeVoidnessPreserves.
  simpl. auto.
Qed.

(* dynamic Function(dynamic) g = func<Object, void>; // Yes *)
Lemma L25 : TypeVoidnessPreserves dt_fun_Object_void dt_fun_dynamic_dynamic.
Proof.
  unfold TypeVoidnessPreserves.
  simpl. auto.
Qed.

(* dynamic Function(dynamic) g = func<void, Object>; // Yes *)
Lemma L26 : TypeVoidnessPreserves dt_fun_void_Object dt_fun_dynamic_dynamic.
Proof.
  unfold TypeVoidnessPreserves.
  simpl. auto.
Qed.

(* Object Function(Object) h = func<void, void>; // No *)
Lemma L27 : ~(TypeVoidnessPreserves dt_fun_void_void dt_fun_Object_Object).
Proof.
  unfold TypeVoidnessPreserves.
  simpl. unfold not. intros. inversion H. inversion H3.
Qed.

(* Object Function(Object) h = func<dynamic, void>; // No *)
Lemma L28 : ~(TypeVoidnessPreserves dt_fun_dynamic_void dt_fun_Object_Object).
Proof.
  unfold TypeVoidnessPreserves.
  simpl. unfold not. intros. inversion H.
  inversion H3.
Qed.

(* Object Function(Object) h = func<void, dynamic>; // Yes *)
Lemma L29 : TypeVoidnessPreserves dt_fun_void_dynamic dt_fun_Object_Object.
Proof.
  unfold TypeVoidnessPreserves.
  simpl. auto.
Qed.

(* Object Function(Object) h = func<Object, Object>; // Yes *)
Lemma L30 : TypeVoidnessPreserves dt_fun_Object_Object dt_fun_Object_Object.
Proof.
  unfold TypeVoidnessPreserves.
  simpl. auto 7.
Qed.

(* Object Function(Object) h = func<Object, void>; // No *)
Lemma L31 : ~(TypeVoidnessPreserves dt_fun_Object_void dt_fun_Object_Object).
Proof.
  unfold TypeVoidnessPreserves.
  simpl. unfold not. intros. inversion H.
  inversion H3.
Qed.

(* Object Function(Object) h = func<void, Object>; // Yes *)
Lemma L32 : TypeVoidnessPreserves dt_fun_void_Object dt_fun_Object_Object.
Proof.
  unfold TypeVoidnessPreserves.
  simpl. auto 7.
Qed.

(* -------------------- Test cases using NotVoidAssignable -------------------- *)

(* A<Object> x = new A<void>(); // No *)
Lemma L33 : NotVoidAssignable dt_A_void dt_A_Object.
Proof.
  apply nva_class. unfold ct_A_void.
  apply nvact_upcast with (args1 := dt_void :: nil).
      apply dsscts_cons.
        apply dscts_first. apply dsct_args. apply dsp_cons.
          apply ds_Object.
        apply dsp_nil.
      apply dsscts_cons.
        apply dscts_rest. apply dscts_first. auto.
      apply dsscts_nil.
    apply ctn_first.
  apply nvap_cons_first. apply nva_base; discriminate.
Qed.

(* A<dynamic> x = new A<void>(); // Yes *)
Lemma L34 : ~(NotVoidAssignable dt_A_void dt_A_dynamic).
Proof.
  unfold not. intros. inversion H. inversion H2.
    subst. unfold ct_A_void in *.
    assert (args1 = dt_void :: nil).
      inversion H8.
        reflexivity.
      contradiction H6. reflexivity.
    subst args1. inversion H9.
      inversion H1. contradiction H10. reflexivity.
    inversion H1.
  unfold ct_A_dynamic in *.
  assert (args2 = dt_dynamic :: nil).
    inversion H8.
      reflexivity.
    contradiction H15. reflexivity.
  subst args2. inversion H9.
    inversion H11. apply H16. reflexivity.
  inversion H11.
Qed.

(* A<Object> x = new A<dynamic>(); // Yes *)
Lemma L35 : ~(NotVoidAssignable dt_A_void dt_A_dynamic).
Proof.
  unfold not. intros. inversion H. inversion H2; subst.
    unfold ct_A_void in *.
    assert (args1 = dt_void :: nil).
      inversion H8.
        reflexivity.
      contradiction H6. reflexivity.
    subst args1. inversion H9.
      inversion H1. apply H10. reflexivity.
    inversion H1.
  assert (args2 = dt_dynamic :: nil).
    inversion H8.
      reflexivity.
    contradiction H7. reflexivity.
  subst args2.
  inversion H9.
    inversion H1. apply H10. reflexivity.
  inversion H1.
Qed.

(* A<void> x = new A<dynamic>(); // voidV = dynamicV, yes *)
Lemma L36 : ~(NotVoidAssignable dt_A_dynamic dt_A_void).
Proof.
  unfold not. intros. inversion H. inversion H2; subst; unfold ct_A_dynamic in *.
    assert (args1 = dt_dynamic :: nil).
      inversion H8.
        reflexivity.
      contradiction H6. reflexivity.
    subst args1. inversion H9.
      inversion H1.
    inversion H1.
  assert (args2 = dt_void :: nil).
    inversion H8.
      reflexivity.
    contradiction H7. reflexivity.
  subst args2. inversion H9.
    inversion H1.
  inversion H1.
Qed.

(* A<void> x = new A<Object>(); // voidV = objectV, Yes *)
Lemma L37 : ~(NotVoidAssignable dt_A_Object dt_A_void).
Proof.
  unfold not. intros. inversion H. inversion H2; subst; unfold ct_A_Object in *.
    assert (args1 = dt_Object :: nil).
      inversion H8.
        reflexivity.
      contradiction H6. reflexivity.
    subst args1. inversion H9.
      inversion H1.
    inversion H1.
  assert (args2 = dt_void :: nil).
    inversion H8.
      reflexivity.
    contradiction H7. reflexivity.
  subst args2. inversion H9.
    inversion H1.
  inversion H1.
Qed.

(* dynamic x = new A<void>(); // Yes *)
Lemma L38 : ~(NotVoidAssignable dt_A_void dt_dynamic).
Proof.
  unfold not. intros. inversion H.
Qed.

(* Object x = new A<void>(); // Yes *)
Lemma L39 : ~(NotVoidAssignable dt_A_void dt_Object).
Proof.
  unfold not. intros. inversion H. inversion H2; subst; unfold ct_A_void in *.
    assert (args1 = nil).
      inversion H9.
    subst args1. inversion H9.
  inversion H8. inversion H10.
Qed.

(* Iterable<void> x = new List<void>(); // Yes *)
Lemma L40 : ~(NotVoidAssignable dt_List_void dt_Iterable_void).
Proof.
  unfold not. intros. inversion H. inversion H2; subst; unfold ct_List_void in *.
    assert (args1 = dt_void :: nil).
      inversion H8. inversion H10.
        reflexivity.
      inversion H17. inversion H24.
    subst args1. inversion H9.
      inversion H1. apply H6. reflexivity.
    inversion H1.
  inversion H8. inversion H10. inversion H17.
Qed.

(* List<void> x = new Iterable<void>(); // Yes *)
Lemma L41 : ~(NotVoidAssignable dt_Iterable_void dt_List_void).
Proof.
  unfold not. intros. inversion H. inversion H2; subst; unfold ct_Iterable_void in *.
    inversion H8. inversion H10. inversion H17.
  assert (args2 = dt_void :: nil).
    inversion H8. inversion H10.
      reflexivity.
    contradiction H16. reflexivity.
  subst args2. inversion H9.
    inversion H1. apply H7. reflexivity.
  inversion H1.
Qed.

(* Iterable<Object> x = new List<void>(); // No *)
Lemma L42 : NotVoidAssignable dt_List_void dt_Iterable_Object.
Proof.
  apply nva_class. apply nvact_upcast with (args1 := dt_void :: nil).
      apply dsscts_cons.
        apply dscts_rest. apply dscts_first. apply dsct_args. apply dsp_cons.
          auto.
        auto.
      apply dsscts_cons.
        apply dscts_rest. apply dscts_rest. apply dscts_first. auto.
      auto.
    apply ctn_rest.
      discriminate.
    apply ctn_first.
  apply nvap_cons_first. apply nva_base.
    discriminate.
  discriminate.
Qed.

(* List<Object> x = new Iterable<void>(); // No *)
Lemma L43 : NotVoidAssignable dt_Iterable_void dt_List_Object.
Proof.
  apply nva_class. apply nvact_downcast with (args2 := dt_Object :: nil).
      apply dsscts_cons.
        apply dscts_rest. apply dscts_first. apply dsct_args. auto.
      apply dsscts_cons.
        apply dscts_rest. apply dscts_rest. apply dscts_first. apply dsct_args. auto.
      auto.
    apply ctn_rest.
      discriminate.
    apply ctn_first.
  apply nvap_cons_first. apply nva_base.
    discriminate.
  discriminate.
Qed.

(* void Function(void) f = func<dynamic, dynamic>; // Yes!! void-to-dynamic is OK! *)
Lemma L44 : ~(NotVoidAssignable dt_fun_dynamic_dynamic dt_fun_void_void).
Proof.
  unfold not. intros. inversion H.
    inversion H2; subst; unfold dt_fun_dynamic_dynamic in *. inversion H5.
  inversion H5.
    inversion H7. apply H12. reflexivity.
  inversion H7. 
Qed.

(* void Function(void) f = func<dynamic, void>; // Yes!! void-to-dynamic is OK! *)
Lemma L45 : ~(NotVoidAssignable dt_fun_dynamic_void dt_fun_void_void).
Proof.
  unfold not. intros. inversion H.
    inversion H2; subst; unfold dt_fun_dynamic_void in *.
    inversion H5. apply H0; reflexivity.
  inversion H5.
    inversion H7. apply H12. reflexivity.
  inversion H7.
Qed.

(* void Function(void) f = func<void, dynamic>; // Yes *)
Lemma L46 : ~(NotVoidAssignable dt_fun_void_dynamic dt_fun_void_void).
Proof.
  unfold not. intros. inversion H.
    inversion H2; subst; unfold dt_fun_void_dynamic in *.
    inversion H5.
  inversion H5.
    inversion H7. apply H11. reflexivity.
  inversion H7.
Qed.

(* void Function(void) f = func<Object, Object>; // No *)
Lemma L47 : NotVoidAssignable dt_fun_Object_Object dt_fun_void_void.
Proof.
  apply nva_function_arg.
    unfold DartAssignable. left. apply ds_function.
      apply ds_void.
    apply dsp_cons.
      apply ds_Object.
    auto.
  apply nvap_cons_first. apply nva_base.
    discriminate.
  discriminate.
Qed.

(* void Function(void) f = func<Object, void>; // No *)
Lemma L48 : NotVoidAssignable dt_fun_Object_void dt_fun_void_void.
Proof.
  apply nva_function_arg.
    unfold DartAssignable. left. apply ds_function.
      apply ds_void.
    apply dsp_cons.
      apply ds_Object.
    auto.
  apply nvap_cons_first. apply nva_base.
    discriminate.
  discriminate.
Qed.

(* void Function(void) f = func<void, Object>; // Yes *)
Lemma L49 : ~(NotVoidAssignable dt_fun_void_Object dt_fun_void_void).
Proof.
  unfold not. intros. inversion H.
    inversion H2; subst; unfold dt_fun_void_Object in *.
    inversion H5.
  inversion H5.
    inversion H7. apply H11. reflexivity.
  inversion H7.
Qed.

(* dynamic Function(dynamic) g = func<void, void>; // Yes *)
Lemma L50 : ~(NotVoidAssignable dt_fun_void_void dt_fun_dynamic_dynamic).
Proof.
  unfold not. intros. inversion H.
    inversion H3; subst; unfold dt_fun_void_void in *.
      inversion H5. apply H1. reflexivity.
    inversion H5. apply H1. reflexivity.
  inversion H5. inversion H7. inversion H7.
Qed.

(* dynamic Function(dynamic) g = func<dynamic, void>; // Yes *)
Lemma L51 : ~(NotVoidAssignable dt_fun_dynamic_void dt_fun_dynamic_dynamic).
Proof.
  unfold not. intros. inversion H.
    inversion H3; subst; unfold dt_fun_dynamic_void in *.
      inversion H5. apply H1. reflexivity.
    inversion H5. apply H1. reflexivity.
  inversion H5.
    inversion H7.
  inversion H7.
Qed.

(* dynamic Function(dynamic) g = func<void, dynamic>; // Yes *)
Lemma L52 : ~(NotVoidAssignable dt_fun_void_dynamic dt_fun_dynamic_dynamic).
Proof.
  unfold not. intros. inversion H.
    inversion H3; subst; unfold dt_fun_void_dynamic in *.
      inversion H5.
    inversion H5.
  inversion H5.
    inversion H7.
  inversion H7.
Qed.

(* dynamic Function(dynamic) g = func<Object, Object>; // Yes *)
Lemma L53 : ~(NotVoidAssignable dt_fun_Object_Object dt_fun_dynamic_dynamic).
Proof.
  unfold not. intros. inversion H.
    inversion H3; subst; unfold dt_fun_Object_Object in *.
      inversion H5.
    inversion H5.
  inversion H5.
    inversion H7. inversion H7.
Qed.

(* dynamic Function(dynamic) g = func<Object, void>; // Yes *)
Lemma L54 : ~(NotVoidAssignable dt_fun_Object_void dt_fun_dynamic_dynamic).
Proof.
  unfold not. intros. inversion H.
    inversion H3; subst; unfold dt_fun_Object_void in *.
      inversion H5. apply H1. reflexivity.
    inversion H5. apply H1. reflexivity.
  inversion H5.
    inversion H7.
  inversion H7.
Qed.

(* dynamic Function(dynamic) g = func<void, Object>; // Yes *)
Lemma L55 : ~(NotVoidAssignable dt_fun_void_Object dt_fun_dynamic_dynamic).
Proof.
  unfold not. intros. inversion H.
    inversion H3; subst; unfold dt_fun_void_Object in *.
      inversion H5.
    inversion H5.
  inversion H5.
    inversion H7.
  inversion H7.
Qed.

(* Object Function(Object) h = func<void, void>; // No *)
Lemma L56 : NotVoidAssignable dt_fun_void_void dt_fun_Object_Object.
Proof.
  apply nva_function_ret.
    unfold DartAssignable. left. apply ds_function.
      apply ds_Object.
    apply dsp_cons.
      apply ds_void.
    auto.
  apply nva_base; discriminate. 
Qed.

(* Object Function(Object) h = func<dynamic, void>; // No *)
Lemma L57 : NotVoidAssignable dt_fun_dynamic_void dt_fun_Object_Object.
Proof.
  apply nva_function_ret.
    unfold DartAssignable. left. apply ds_function.
      apply ds_Object.
    apply dsp_cons.
      apply ds_dynamic.
    auto.
  apply nva_base; discriminate.
Qed.

(* Object Function(Object) h = func<void, dynamic>; // Yes *)
Lemma L58 : ~(NotVoidAssignable dt_fun_void_dynamic dt_fun_Object_Object).
Proof.
  unfold not. intros. inversion H.
    inversion H3; subst; unfold dt_fun_void_dynamic in *.
      inversion H5.
    inversion H5.
  inversion H5.
    inversion H7.
  inversion H7.
Qed.

(* Object Function(Object) h = func<Object, Object>; // Yes *)
Lemma L59 : ~(NotVoidAssignable dt_fun_Object_Object dt_fun_Object_Object).
Proof.
  unfold not. intros. inversion H.
    inversion H3; subst; unfold dt_fun_Object_Object in *.
      inversion H5. inversion H2.
        inversion H12.
      inversion H12; subst.
    inversion H5. inversion H2.
      inversion H12.
    inversion H12.
  inversion H5.
    inversion H7. inversion H13.
      inversion H20.
    inversion H20.
  inversion H7.
Qed.

(* Object Function(Object) h = func<Object, void>; // No *)
Lemma L60 : NotVoidAssignable dt_fun_Object_void dt_fun_Object_Object.
Proof.
  apply nva_function_ret.
    unfold DartAssignable. left. apply ds_function.
      apply ds_Object.
    apply dsp_cons.
      apply ds_Object.
    auto.
  apply nva_base; discriminate.
Qed.

(* Object Function(Object) h = func<void, Object>; // Yes *)
Lemma L61 : ~(NotVoidAssignable dt_fun_void_Object dt_fun_Object_Object).
Proof.
  unfold not. intros. inversion H.
    inversion H3; subst; unfold dt_fun_void_Object in *.
      inversion H5. inversion H2.
        inversion H12.
      inversion H12.
    inversion H5. inversion H2.
      inversion H12.
    inversion H12.
  inversion H5.
    inversion H7.
  inversion H7.
Qed.