(* HF *) (* Aritmetikai kifejezesnyelv es denotacios szemantika, pelda kiertekelesek bin_tree, height, sum aexp, aeval, leaves_cnt, height *) From Coq Require Import Init.Nat. Check nat. Check 5. Compute 1 + 3. (* absztrakcios szintek*) (*a ::= n | a1 + a2 | a1 - a2*) (*a ::= alit(n) | plus(a1,a2) | sub(a1,a2)*) Inductive AExp : Type := | ALit (n : nat) | APlus (a1 a2 : AExp) | ASub (a1 a2 : AExp) . (* Checkek *) (* (5 + 7) - 42 *) Check (ASub (APlus (ALit 5) (ALit 7)) (ALit 42)). (* Ird le, mint AExp elemet! + / \ + 3 / \ 1 2 *) Definition t1 : AExp := (* Ird le, mint AExp elemet! + / \ 1 + / \ 2 3 *) Definition t1' : AExp := (* Ird le, mint AExp elemet! + / \ 3 + / \ 1 2 *) Definition t1'' : AExp := (* Ird le, mint AExp elemet! - / \ + + / \ /\ 1 2 + 3 / \ 4 5 *) Definition t2 : AExp := (* Rajzold le! *) Definition t3 := ASub (APlus (ALit 5) (ALit 7)) (ALit 42). Definition t3' := ASub (APlus (ALit 5) (ALit 7)) (ALit 42). Compute 5 - 15. (* notation AExp-re is *) Fixpoint aeval (a : AExp) : nat := match a with | ALit n => n | APlus a1 a2 => aeval a1 + aeval a2 | ASub a1 a2 => aeval a1 - aeval a2 end. Compute aeval t1. Compute aeval t2. Fixpoint leaves_count (a : AExp) : nat := match a with | ALit n => 1 | APlus a1 a2 => leaves_count a1 + leaves_count a2 | ASub a1 a2 => leaves_count a1 + leaves_count a2 end . Compute leaves_count t1. Compute leaves_count t3'. From Coq Require Import Arith.PeanoNat. Lemma leaf_l_r: forall a1 a2 : AExp, leaves_count (APlus a1 a2) = leaves_count (APlus a2 a1). Lemma leaf_l_r2: forall a1 a2 : AExp, leaves_count (APlus a1 a2) = leaves_count (APlus a2 a1).