(** Contrução do conjunto que contém os dias da semana como elementos *) Inductive Sem := | domingo: Sem | segunda_feira: Sem | terca_feira: Sem | quarta_feira: Sem | quinta_feira: Sem | sexta_feira: Sem | sabado: Sem. Print Sem_ind. (** A seguir provaremos que a soma dos n primeiros números ímpares é igual a n*n. *) Print nat. Print nat_ind. Inductive lprop := | var: nat -> lprop | bot: lprop | dis: lprop -> lprop -> lprop | con: lprop -> lprop -> lprop | imp: lprop -> lprop -> lprop | neg: lprop -> lprop. Print lprop_ind. Require Import Lia. (** A função [msum] a seguir, computa a soma dos n primeiros números ímpares. *) Fixpoint msum (n:nat) := match n with | 0 => 0 | S k => (msum k) + (2*k+1) end. Eval compute in (msum 1). Eval compute in (msum 2). Eval compute in (msum 3). Eval compute in (msum 4). (** O lema a seguir, expressa a propriedade de que a soma dos n primeiros números ímpares é igual a n*n. *) Lemma msum_square: forall n, msum n = n*n. Proof. induction n as [| k]. - reflexivity. - simpl msum. rewrite IHk. lia. Qed. (** Prove que a soma dos n primeiros números naturais é igual a n*(S n)/2. Inicialmente definimos o somatório [sum] que retorna a soma dos n primeiros números naturais. *) Fixpoint nsum (n:nat) := match n with | 0 => 0 | S k => (nsum k) + n end. Eval compute in (nsum 1). Eval compute in (nsum 2). Eval compute in (nsum 3). Lemma nsum_prop: forall n, 2*nsum n = n*(S n). Proof. induction n as [| k]. - reflexivity. - simpl nsum. rewrite PeanoNat.Nat.mul_add_distr_l. rewrite IHk. lia. Qed. Require Import Arith. Fixpoint psum (n:nat) := match n with | 0 => 1 | S k => (psum k) + 2^n end. Eval compute in (psum 1). Eval compute in (psum 2). Lemma psum_prop: forall n, psum n = 2^(S n) - 1. Proof. induction n as [| k]. - reflexivity. - simpl psum. rewrite IHk. simpl. repeat rewrite Nat.add_0_r. lia. Qed. Print list. Check list_ind. Lemma soma_concat: forall l1 l2: list nat, length(l1 ++l2) = (length l1) + (length l2). Proof. Admitted.