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 : list A -> prop by is_list nil; is_list (X :: L) := is_list L. Theorem is_list_inst[A,B] : forall (L:B -> list A) V, nabla (x:B), is_list (L x) -> is_list (L V). Define list_length : list A -> nat -> prop by list_length nil z; list_length (M :: ML) (s N) := list_length ML N. Define append : list A -> list A -> list A -> prop by append nil L L; append (X :: L1) L2 (X :: L3) := append L1 L2 L3. Theorem append_refl[A] : forall (L:list A), is_list L -> append L nil L. Theorem append_exists[A] : forall (L1:list A) L2, is_list L1 -> exists L3, append L1 L2 L3. Theorem append_result_islist[A] : forall (L1:list A) L2 L, is_list L2 -> append L1 L2 L -> is_list L. Theorem append_arg2_islist[A] : forall (L1:list A) L2 L, is_list L -> append L1 L2 L -> is_list L2. Theorem append_arg1_islist[A] : forall (L1:list A) L2 L, append L1 L2 L -> is_list L1. Theorem append_prune[A,B] : forall (L1:list A) L2 L3, nabla (n:B), append L1 L2 (L3 n) -> exists L3', L3 = y\L3'. Define subset : list A -> list A -> prop by subset nil L; subset (X :: L1) L2 := member X L2 /\ subset L1 L2. Theorem subset_add[A] : forall (L:list A) L' X, subset L L' -> subset L (X :: L'). Theorem subset_refl[A] : forall (L:list A), is_list L -> subset L L. Theorem subset_mem_trans[A] : forall L1 L2 (X:A), subset L1 L2 -> member X L1 -> member X L2. Theorem subset_trans[A] : forall (L1:list A) L2 L3, subset L1 L2 -> subset L2 L3 -> subset L1 L3. Theorem subset_extend[A] : forall L L' (X:A), subset L L' -> subset (X :: L) (X :: L'). Theorem append_sub1[A] : forall (L1:list A) L2 L, append L1 L2 L -> subset L1 L. Theorem append_sub2[A] : forall (L1:list A) L2 L, is_list L2 -> append L1 L2 L -> subset L2 L. Theorem append_subset_trans[A] : forall (L1:list A) L2 L L', append L1 L2 L -> subset L1 L' -> subset L2 L' -> subset L L'. Theorem append_append_subset_trans[A] : forall (L1:list A) 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.% rev Theorem rev_det[A] : forall (L1:list A) L2 L3 L3', {rev L1 L2 L3} -> {rev L1 L2 L3'} -> L3 = L3'. Theorem rev_prune[A,B] : forall (L1:list A) L2 L3, nabla (x:B), {rev L1 L2 (L3 x)} -> exists L3', L3 = x\L3'. % subset for specifications Define ssubset : list A -> list A -> prop by ssubset nil L; ssubset (X :: L1) L2 := {memb X L2} /\ ssubset L1 L2. Theorem appd_refl_eq[A] : forall (L1:list A) L2, {appd L1 nil L2} -> L1 = L2. Theorem ssubset_add[A] : forall (L:list A) L' X, ssubset L L' -> ssubset L (X :: L'). Theorem ssubset_refl[A] : forall (L:list A), is_list L -> ssubset L L. Theorem ssubset_mem_trans[A] : forall (L1:list A) L2 X, ssubset L1 L2 -> {memb X L1} -> {memb X L2}. Theorem ssubset_trans[A] : forall (L1:list A) L2 L3, ssubset L1 L2 -> ssubset L2 L3 -> ssubset L1 L3. Theorem ssubset_extend[A] : forall (L:list A) L' X, ssubset L L' -> ssubset (X :: L) (X :: L'). % Pruning lemmas Theorem member_prune[A,B] : forall M (L:list A), nabla (x:B), member (M x) L -> exists M', M = y\M'. Theorem memb_prune[A,B] : forall M (L:list A), nabla (x:B), {memb (M x) L} -> exists M', M = y\M'. % Structural definitions for the source and target languages Define name : A -> prop by nabla n, name n. % Lemmas of combine Theorem combine_subset[A] : forall L1 L2 (L:list A), is_list L -> {combine L1 L2 L} -> ssubset L1 L /\ ssubset L2 L.induction on 2. intros. case H2. split. search. backchain ssubset_refl. apply IH to _ H4. apply ssubset_mem_trans to H6 H3. search. case H1. apply IH to _ H3. split. backchain ssubset_extend. backchain ssubset_add.Theorem combine_sub1[A] : forall (L1:list A) L2 L, is_list L -> {combine L1 L2 L} -> ssubset L1 L. Theorem combine_sub2[A] : forall (L1:list A) L2 L, is_list L -> {combine L1 L2 L} -> ssubset L2 L. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% Mappings %%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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_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'. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% Application of substitutions %%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Define app_subst : list (map A A) -> B -> B -> prop by app_subst nil M M; nabla x, app_subst (map x V :: ML) (R x) M := app_subst ML (R V) M. Theorem app_subst_det[A,B] : forall (ML:list (map A A)) (M:B) M' M'', app_subst ML M M' -> app_subst ML M M'' -> M' = M''. Theorem app_subst_prune[A,B,C] : forall (ML:list (map A A)) (M:B) M', nabla (x:C), app_subst ML M (M' x) -> exists M'', M' = y\M''. Theorem app_subst_inst[A,B,C] : forall (ML:list (map A A)) (M1:C) (M2:C -> B) M1' M2', nabla (x:C), app_subst ML M1 M1' -> app_subst ML (M2 x) (M2' x) -> app_subst ML (M2 M1) (M2' M1'). % Application of substitutions to a list Define app_subst_list : list (map A A) -> list B -> list B -> prop by app_subst_list nil L L; nabla x, app_subst_list (map x V :: ML) (L x) L' := app_subst_list ML (L V) L'. Theorem app_subst_islist_trans[A,B] : forall (L:list B) L' (ML:list (map A A)), is_list L -> app_subst_list ML L L' -> is_list L'.induction on 2. intros. case H2. search. apply is_list_inst to H1 with V = V. apply IH to H4 H3. search.Theorem app_subst_list_nil_comm[A,B] : forall (ML:list (map A A)) (M:list B), app_subst_list ML nil M -> M = nil. Theorem app_subst_list_comm1[A,B] : forall (ML:list (map A A)) X (L:list B) M, app_subst_list ML (X :: L) M -> exists X' L', M = X' :: L' /\ app_subst ML X X' /\ app_subst_list ML L L'. Theorem app_subst_list_comm2[A,B] : forall (ML:list (map A A)) X (L:list B) M, is_list M -> app_subst_list ML M (X :: L) -> exists X' L', M = X' :: L' /\ app_subst ML X' X /\ app_subst_list ML L' L.induction on 2. intros. case H2. search. apply is_list_inst to H1 with V = V. case H1. apply IH to _ H3. apply IH to H4 H3. search.Theorem app_subst_list_compose[A,B] : forall (ML:list (map A A)) X X' (L:list B) L', app_subst ML X X' -> app_subst_list ML L L' -> app_subst_list ML (X :: L) (X' :: L'). Theorem app_subst_list_prune[A,B,C] : forall (ML:list (map A A)) (M:list B) M', nabla (x:C), app_subst_list ML M (M' x) -> exists M'', M' = y\M''.