proposition: Theorem find_expr_correct : forall e vars lp lc, match find_expr e vars lp lc with | Some n => nth n (lp ++ map Evar (seq 0 vars) ++ lc) (Econst (Int 0)) = e | None => True end.
proof: Proof. intros e vars lp lc. assert (H1: forall l n, match find_expr_aux e n l with | Some k => (n <= k < n + length l)%nat /\ nth (k - n) l (Econst (Int 0)) = e | None => True end). induction l as [|h t IH]. easy. intros n. simpl find_expr_aux. generalize (internal_expr_dec_bl e h). destruct expr_beq. intros H. split. simpl. lia. rewrite Nat.sub_diag. now rewrite H. intros _. specialize (IH (S n)). revert IH. destruct find_expr_aux as [k|] ; try easy. intros [H1 H2]. split. simpl. lia. replace (k - n)%nat with (S (k - S n))%nat by lia. easy. unfold find_expr. set (foo := match find_expr_aux e 0%nat lp with | Some n => Some n | None => find_expr_aux e (length lp + vars)%nat lc end). assert (H2: match foo with | Some n => nth n (lp ++ map Evar (seq 0 vars) ++ lc) (Econst (Int 0)) = e | None => True end). unfold foo. clear foo. generalize (H1 lp 0%nat). destruct find_expr_aux as [n1|]. rewrite Nat.add_0_l, Nat.sub_0_r. intros [H2 H3]. now rewrite app_nth1. intros _. specialize (H1 lc (length lp + vars)%nat). revert H1. destruct find_expr_aux as [n2|] ; try easy. intros [H1 H2]. rewrite -> app_nth2 by lia. rewrite app_nth2 ; rewrite map_length, seq_length. now rewrite <- Nat.sub_add_distr. lia. destruct e as [n|o|o n1|o n1 n2] ; simpl ; try easy. destruct (Nat.ltb_spec n vars) as [H|H] ; try easy. rewrite app_nth2 by apply Nat.le_add_r. rewrite Nat.add_comm, Nat.add_sub. rewrite app_nth1. rewrite nth_indep with (d' := Evar 0). now rewrite map_nth, seq_nth. now rewrite map_length, seq_length. now rewrite map_length, seq_length. Qed.
imports: Coq(ZArith Reals List Psatz) Xreal Tree