Executable Specification

[View trans]

Reasoning

[View util]

Click on a command or tactic to see a detailed view of its use.

Specification "trans".

%%%%%%% Arithmetics %%%%%%%%%%%

Theorem add_det : forall N1 N2 N3 N3',
  {add N1 N2 N3} -> {add N1 N2 N3'} -> N3 = N3'.

Define le : nat -> nat -> prop by
  le N1 N2 := exists N, {add N1 N N2}.

Define lt : nat -> nat -> prop by
  lt N1 N2 := exists N, {add N1 (s N) N2}.

Theorem lt_to_le : forall N1 N2,
  lt N1 N2 -> le N1 N2.

Theorem le_refl : forall N,
  {is_nat N} -> le N N.

Theorem le_z : forall N,
  le N z -> N = z.

Theorem add_result_isnat : forall N1 N2 N3,
  {is_nat N2} -> {add N1 N2 N3} -> {is_nat N3}.

Theorem add_arg2_isnat : forall N1 N2 N3,
  {is_nat N3} -> {add N1 N2 N3} -> {is_nat N2}.

Theorem add_arg2_det : forall N1 N2 N2' N3,
  {add N1 N2 N3} -> {add N1 N2' N3} -> N2 = N2'.

Theorem add_arg1_isnat: forall N1 N2 N3,
  {add N1 N2 N3} -> {is_nat N1}.

Theorem add_s : forall N1 N2 N3,
  {add N1 N2 N3} -> {add N1 (s N2) (s N3)}.

Theorem add_s_inv : forall N1 N2 N3,
  {add N1 (s N2) (s N3)} -> {add N1 N2 N3}.

Theorem add_z : forall N, 
  {is_nat N} -> {add N z N}.

Theorem add_comm : forall N1 N2 N3,
  {is_nat N3} -> {add N1 N2 N3} -> {add N2 N1 N3}.

Theorem add_assoc : forall N1 N2 N3 N12 N123,
  {add N1 N2 N12} -> {add N12 N3 N123} ->
    exists N23, {add N2 N3 N23} /\ {add N1 N23 N123}.

Theorem add_assoc' : forall N1 N2 N3 N23 N123,
  {add N2 N3 N23} -> {add N1 N23 N123} ->
    exists N12, {add N1 N2 N12} /\ {add N12 N3 N123}.


Theorem le_to_lt : forall N1 N2,
  {is_nat N2} -> le N1 N2 -> N1 = N2 \/ lt N1 N2.

Theorem lt_pred_le : forall I J,
  {is_nat J} -> lt I (s J) -> le I J.

Theorem lt_z_absurd : forall I,
  lt I z -> false.

Theorem le_succ : forall I J,
  le I J -> le I (s J).

Theorem le_extend : forall I J,
  le I J -> le (s I) (s J).

Theorem le_to_lt_s : forall N1 N2,
  le N1 N2 -> lt N1 (s N2).

Theorem le_trans: forall N1 N2 N3,
  le N1 N2 -> le N2 N3 -> le N1 N3.

Theorem lt_le_compose: forall N1 N2 N3,
  lt N1 N2 -> le N2 N3 -> lt N1 N3.
 
Theorem add_result_le_to_arg1_le : forall N1 N2 N2' J K,
  {add N1 N2 J} -> {add N1 N2' K} -> le J K -> le N2 N2'.

Theorem add_le_complement : forall N1 N2 N1' N2' N,
  {is_nat N2} -> le N1 N1' -> {add N1 N2 N} -> {add N1' N2' N} -> le N2' N2.

Theorem k_minus_n1 : forall N1 N2 N3 N23 N123 N K,
  {add N2 N3 N23} -> {add N1 N23 N123} -> {add N123 N K} -> 
    exists K', {add N1 K' K}.

Theorem k_minus_n2 : forall N1 N2 N3 N23 N123 N K,
  {add N2 N3 N23} -> {add N1 N23 N123} -> {add N123 N K} ->
    exists K', {add N2 K' K}.

Theorem k_minus_n12 : forall N1 N2 N3 N23 N123 N K,
  {add N2 N3 N23} -> {add N1 N23 N123} -> {add N123 N K} ->
    exists K' N12, {add N1 N2 N12} /\ {add N3 N K'} /\ {add N12 K' K}.

Theorem sum_complement_to_lt1 : forall N1 N2 N12 K K' N,
  {is_nat N} -> {add N1 N2 N12} -> {add N12 K N} -> {add N1 K' N} -> lt K (s K').

Theorem sum_complement_to_lt2 : forall N1 N2 N12 K K' N,
  {is_nat N} -> {add N1 N2 N12} -> {add N12 K N} -> {add N2 K' N} -> lt K (s K').

Theorem npred_det : forall N N1 N2,
  {npred N N1} -> {npred N N2} -> N1 = N2.

%%%%%%%%%%%%% Lists %%%%%%%%%%%%%%%%
Define is_list : olist -> prop by
  is_list nil;
  is_list (X :: L) := is_list L.

Define append : olist -> olist -> olist -> prop by
  append nil L L;
  append (X :: L1) L2 (X :: L3) := append L1 L2 L3.

Theorem append_refl : forall L,
  is_list L -> append L nil L.

Theorem append_exists : forall L1 L2,
  is_list L1 -> exists L3, append L1 L2 L3.

Theorem append_result_islist : forall L1 L2 L,
  is_list L2 -> append L1 L2 L -> is_list L.

Theorem append_arg2_islist : forall L1 L2 L,
  is_list L -> append L1 L2 L -> is_list L2.

Theorem append_arg1_islist : forall L1 L2 L,
  append L1 L2 L -> is_list L1.


Define subset : olist -> olist -> prop by
   subset nil L;
   subset (X :: L1) L2 := member X L2 /\ subset L1 L2.

Theorem subset_add : forall L L' X,
  subset L L' -> subset L (X :: L').

Theorem subset_refl : forall L,
  is_list L -> subset L L.

Theorem subset_mem_trans : forall L1 L2 X,
  subset L1 L2 -> member X L1 -> member X L2.

Theorem subset_trans : forall L1 L2 L3,
  subset L1 L2 -> subset L2 L3 -> subset L1 L3.

Theorem subset_extend : forall L L' X,
  subset L L' -> subset (X :: L) (X :: L').

Theorem append_sub1 : forall L1 L2 L,
  append L1 L2 L -> subset L1 L.

Theorem append_sub2 : forall L1 L2 L,
  is_list L2 -> append L1 L2 L -> subset L2 L.

Theorem append_subset_trans : forall L1 L2 L L',
  append L1 L2 L -> subset L1 L' -> subset L2 L' -> subset L L'.

Theorem append_append_subset_trans : forall L1 L1' L2 L2' L L',
  is_list L2' -> append L1 L2 L -> append L1' L2' L' -> subset L1 L1' -> subset L2 L2' -> subset L L'.


Define tm_subset : tm_list -> tm_list -> prop by
  tm_subset snil L;
  tm_subset (scons X L1) L2 := {smember X L2} /\ tm_subset L1 L2.

Define is_tm_list : tm_list -> prop by
  is_tm_list snil;
  is_tm_list (scons X L) := is_tm_list L.

Theorem sappend_refl_eq : forall L1 L2,
  {sappend L1 snil L2} -> L1 = L2.

Theorem append_prune_tm : forall L1 L2 L3, nabla (n:tm),
  append L1 L2 (L3 n) -> exists L3', L3 = y\L3'.

Theorem tm_subset_add : forall L L' X,
  tm_subset L L' -> tm_subset L (scons X L').

Theorem tm_subset_refl : forall L,
  is_tm_list L -> tm_subset L L.

Theorem tm_subset_mem_trans : forall L1 L2 X,
  tm_subset L1 L2 -> {smember X L1} -> {smember X L2}.

Theorem tm_subset_trans : forall L1 L2 L3,
  tm_subset L1 L2 -> tm_subset L2 L3 -> tm_subset L1 L3.

Theorem tm_subset_extend : forall L L' X,
  tm_subset L L' -> tm_subset (scons X L) (scons X L').

Define is_tm'_list : tm'_list -> prop by
  is_tm'_list cnil;
  is_tm'_list (ccons X L) := is_tm'_list L.

Theorem is_tm'_list_inst : forall L V, nabla (x:tm'),
  is_tm'_list (L x) -> is_tm'_list (L V).

Define tm'_list_length : tm'_list -> nat -> prop by
  tm'_list_length cnil z;
  tm'_list_length (ccons M ML) (s N) := tm'_list_length ML N.

% Pruning lemmas
Theorem member_prune_tm : forall M L, nabla (x:tm),
  member (M x) L -> exists M', M = y\M'.

Theorem member_prune_tm' : forall M L, nabla (x:tm'),
  member (M x) L -> exists M', M = y\M'.

Theorem mmember_prune_tm : forall M L, nabla (x:tm),
  {mmember (M x) L} -> exists M', M = y\M'.

Theorem mmember_prune_tm' : forall M L, nabla (x:tm'),
  {mmember (M x) L} -> exists M', M = y\M'.



% Structural definitions for the source and target languages
Define name : tm -> prop by
  nabla n, name n.

Define name' : tm' -> prop by
  nabla n, name' n.


% Lemmas of combine
Theorem combine_subset : forall Vs1 Vs2 Vs,
  is_tm_list Vs -> {combine Vs1 Vs2 Vs} -> tm_subset Vs1 Vs /\ tm_subset Vs2 Vs.

Theorem combine_sub1 : forall Vs1 Vs2 Vs,
  is_tm_list Vs -> {combine Vs1 Vs2 Vs} -> tm_subset Vs1 Vs.

Theorem combine_sub2 : forall Vs1 Vs2 Vs,
  is_tm_list Vs -> {combine Vs1 Vs2 Vs} -> tm_subset Vs2 Vs.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% Mappings %%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Mapping of source variables into terms
Kind smap       type.
Kind smap_list  type.
Type smap     tm -> tm -> smap.
Type smnil    smap_list.
Type smcons   smap -> smap_list -> smap_list.

Define smmember: smap -> smap_list -> prop by
  smmember X (smcons X L);
  smmember X (smcons Y L) := smmember X L.

% Mapping of target variables into terms
Kind cmap       type.
Kind cmap_list  type.
Type cmap     tm' -> tm' -> cmap.
Type cmnil    cmap_list.
Type cmcons   cmap -> cmap_list -> cmap_list.

Define cmmember: cmap -> cmap_list -> prop by
  cmmember X (cmcons X L);
  cmmember X (cmcons Y L) := cmmember X L.

% Pruning lemmas
Theorem smmember_prune_tm : forall M L, nabla (x:tm),
  smmember (M x) L -> exists M', M = y\M'.

Theorem cmmember_prune_tm' : forall M L, nabla (x:tm'),
  cmmember (M x) L -> exists M', M = y\M'.

% crev
Theorem crev_det : forall L1 L2 L3 L3',
  {crev L1 L2 L3} -> {crev L1 L2 L3'} -> L3 = L3'.

Theorem crev_prune : forall L1 L2 L3, nabla (x:tm'),
  {crev L1 L2 (L3 x)} -> exists L3', L3 = x\L3'.

% tm'_list_to_tuple
Theorem tm'_list_to_tuple_det : forall FE E E',
  {tm'_list_to_tuple FE E} -> {tm'_list_to_tuple FE E'} -> E = E'.

Theorem tm'_list_to_tuple_exists : forall L,
  is_tm'_list L -> exists E, {tm'_list_to_tuple L E}.

Theorem tm'_list_to_tuple_prune : forall L E, nabla (x:tm'),
  {tm'_list_to_tuple L (E x)} -> exists E', E = y\E'.