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.intros. case H2. apply add_comm to _ H3. case H4. search. apply add_comm to _ H5. case H1. search. search.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'.induction on 1. intros. case H1. case H2. search. case H2. assert le N3 N4. case H3. case H6. search. apply IH to H4 H5 H6. search.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.induction on 3. intros. case H3. apply add_comm to _ H4. search. case H2. case H6. case H4. apply IH to H1 _ H5 H8. search.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}.induction on 2. intros. case H2. apply add_assoc to H1 H3. search. case H3. apply IH to _ H4 _. apply add_s to H6. search.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}.induction on 2. intros. case H2. apply add_assoc to H1 H3. search. case H3. apply IH to _ H4 _. search.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').intros. apply add_assoc to H2 H3. unfold. apply add_arg2_det to H4 H6. apply add_comm to _ H5. backchain add_arg2_isnat. apply add_s to H7. search.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').intros. apply add_comm to _ H2. backchain add_arg1_isnat. apply sum_complement_to_lt1 to _ H5 H3 H4. search.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'.intros. assert subset L1 L'. backchain subset_trans with L2 = L1'. backchain append_sub1. assert subset L2 L'. backchain subset_trans with L2 = L2'. backchain append_sub2. backchain append_subset_trans.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.induction on 2. intros. case H2. split. search. backchain tm_subset_refl. apply IH to _ H4. apply tm_subset_mem_trans to H6 H3. search. case H1. apply IH to _ H3. split. backchain tm_subset_extend. backchain tm_subset_add.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'.