Last change
on this file since 2542 was
2514,
checked in by sacerdot, 7 years ago

All .ma files committed: some of them are just inprogress.

File size:
1.7 KB

Line  

1  include "variants.ma". 

2  

3  coercion sub_expr2 : ∀l:list tag_. Type[0] → Type[0] 

4  ≝ sub_expr on _l: list tag_ to Type[0] → Type[0]. 

5  

6  definition eval_additive_expr: ∀E:Type[0]. (E → nat) → [plus] E → nat ≝ 

7  λE,f,e. 

8  match e return λe. is_in … [plus] e → nat with 

9  [ Plus x y ⇒ λH. f x + f y 

10   _ ⇒ λH:False. ? 

11  ] (se_el_in ?? e). 

12  elim H qed. 

13  

14  definition eval_multiplicative_expr: ∀E:Type[0]. (E → nat) → [mul] E → nat ≝ 

15  λE,f,e. 

16  match e return λe. is_in … [mul] e → nat with 

17  [ Mul x y ⇒ λH. f x * f y 

18   _ ⇒ λH:False. ? 

19  ] (se_el_in ?? e). 

20  elim H qed. 

21  

22  definition eval_additive_multiplicative_expr: ∀E:Type[0]. (E → nat) → [plus;mul] E → nat ≝ 

23  λE,f,e. 

24  match e return λe. is_in … [plus;mul] e → nat with 

25  [ Plus x y ⇒ λH. eval_additive_expr … f (Plus ? x y) 

26   Mul x y ⇒ λH. eval_multiplicative_expr E f (Mul ? x y) 

27   _ ⇒ λH:False. ? 

28  ] (se_el_in ?? e). 

29  [2,3: %  elim H] 

30  qed. 

31  

32  definition eval_additive_multiplicative_constant_expr: ∀E:Type[0]. (E → nat) → [plus;mul;num] E → nat ≝ 

33  λE,f,e. 

34  match e return λe. is_in … [plus;mul;num] e → nat with 

35  [ Plus x y ⇒ λH. eval_additive_expr … f (Plus ? x y) 

36   Mul x y ⇒ λH. eval_multiplicative_expr E f (Mul ? x y) 

37   Num n ⇒ λH. n 

38  ] (se_el_in ?? e). 

39  % qed. 

40  

41  (*CSC: not accepted :( 

42  inductive expr_no_const : Type[0] ≝ K : [plus;mul] expr_no_const → expr_no_const. 

43  *) 

44  

45  inductive final_expr : Type[0] ≝ K : expr final_expr → final_expr. 

46  

47  coercion K. 

48  

49  let rec eval_final_expr e on e : nat ≝ 

50  match e with 

51  [ K e' ⇒ eval_additive_multiplicative_constant_expr final_expr eval_final_expr e']. 

52  cases e' try #x try #y % 

53  qed. 

54  

55  example test: eval_final_expr (K (Mul ? (Num ? 2) (Num ? 3))) = 6. 

56  % qed. 

Note: See
TracBrowser
for help on using the repository browser.