max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
23964 commits 1 branch 0 tags 5.3 GiB
Commit graph

3215 commits

Author SHA1 Message Date
Leonardo de Moura
6eeccdd675 test: for field auto implicit bound feature 2021-02-20 07:52:42 -08:00
Leonardo de Moura
e1f6965266 feat: allow user to define rewrite lemmas with (local) match expressions 2021-02-19 15:18:19 -08:00
Leonardo de Moura
d493e700cc fix: matchUnit simplification 2021-02-19 13:51:08 -08:00
Leonardo de Moura
2861f71c61 feat: add option autoLift 2021-02-19 11:02:58 -08:00
Leonardo de Moura
c06ca8304d fix: test 2021-02-18 16:54:45 -08:00
Leonardo de Moura
df8634e9ad fix: assertAfter 2021-02-17 13:52:43 -08:00
Leonardo de Moura
bb2ca97df9 refactor: add options for controlling whether variables are included or not at mkLambdaFVars and mkForallFVars 2021-02-17 13:49:27 -08:00
Leonardo de Moura
c97ae92afe chore: cleanup 2021-02-17 13:03:24 -08:00
Leonardo de Moura
79a4aebf96 feat: add byCases tactic 2021-02-17 13:03:24 -08:00
Leonardo de Moura
08927f1e66 test: tactic framework and AC by reflection 2021-02-17 13:03:24 -08:00
Leonardo de Moura
1a7535263e fix: unfolding class projections at simp 2021-02-16 17:55:57 -08:00
Leonardo de Moura
5f80659b45 fix: unfold constants at simp 2021-02-16 15:42:31 -08:00
Leonardo de Moura
5e24da0c2e fix: simp argument issue 
See new test.
 2021-02-16 13:12:57 -08:00
Leonardo de Moura
d1009e8405 chore: add simp lemmas, theorem naming convention 2021-02-16 11:53:49 -08:00
Leonardo de Moura
242a8dcfbf test: simp 2021-02-15 17:09:51 -08:00
Leonardo de Moura
e97df2f61b feat: functions to unfold at simp 2021-02-15 15:32:25 -08:00
Leonardo de Moura
1c5de9842d feat: use decide at simp 2021-02-15 13:08:45 -08:00
Leonardo de Moura
9528c1abd7 chore: add basic simp lemmas 
TODO: consistent naming convention for theorems.

cc @Kha
 2021-02-15 11:32:19 -08:00
Leonardo de Moura
3bc5b89ac3 test: add if p x then .. else .. example 
cc @Kha
 2021-02-14 11:44:10 -08:00
Leonardo de Moura
0787886cea feat: improve simp local lemma elaboration 2021-02-13 18:55:19 -08:00
Leonardo de Moura
2944da2a0b feat: use simp itself as default method for discharging hypotheses of conditional rewriting rules 2021-02-13 18:55:19 -08:00
Leonardo de Moura
21878030d1 fix: fixes #310 
@Kha I implemented the following approach:

- Error if user tries to revert `auxDecl`.
- Clear any `auxDecl` that depends on variables being reverted by the user.
 2021-02-12 18:14:42 -08:00
Sebastian Ullrich
75243e7f24 feat: change back seqLeft/Right signature 
This was originally changed for the sake of `do`, which does not depend on it anymore
 2021-02-12 17:08:06 -08:00
Leonardo de Moura
c64d053f9e test: ite and dite congr test 2021-02-12 16:52:56 -08:00
Leonardo de Moura
8b3c61dbb0 fix: checkAssignment 2021-02-11 16:56:32 -08:00
Leonardo de Moura
16429e393d test: add dep hd test 
It has been reported in the general channel that this example
generates problems for the Lean 3 elaborator.
 2021-02-08 11:26:23 -08:00
Leonardo de Moura
4e4194af41 feat: add autoBoundImplicit support for structure fields 2021-02-06 17:58:29 -08:00
Leonardo de Moura
023d7605fb feat: add "transitivity" to "has_loose_bvars_in_domain" 2021-02-06 17:42:38 -08:00
Leonardo de Moura
78fb026201 test: add test for issue #305 
Issue #305 was fixed by previous commits submitted today for problems
exposed by the `for in` notation based on typeclasses :)

closes #305
 2021-02-05 18:15:11 -08:00
Leonardo de Moura
83775b08cb fix: whnfCore not expanding delayed assignments 2021-02-05 15:14:12 -08:00
Leonardo de Moura
8c0346f00c feat: improve binrel! macro 2021-02-05 13:28:57 -08:00
Leonardo de Moura
10a10b38d8 fix: fixes #303 2021-02-05 07:53:18 -08:00
Leonardo de Moura
53539b1dff chore: use polymorphic method forIn 2021-02-04 18:13:01 -08:00
Leonardo de Moura
d494756d00 fix: inline loop 2021-02-04 17:17:51 -08:00
Leonardo de Moura
729047b5a2 feat: auto bound implicit at constructors 
@Kha This commit adds auto bound implicits to constructors.
I was excited until I tried to define the `Bigstep` type again without
`autoBoundImplicitLocal`, and found small typos.
Example, I had
```
  | ifTrue  : eval σ₁ b = true  → Bigstep (c₁, σ₁) σ₂ t → Bigstep (cond b c₁ c₂, σ₁) σ₂ (t₁ + 1)
```
where `t₁` should be `t`, but the declaration was accepted. I am
wondering whether Isabelle performs some kind of sanity checking,
and/or enforces rules such as: auto-bound implicits may only be
introduced by hypotheses.
Note that this is not an issue for definitions, because the body of
the definition will probably not type check when we have this kind of
typo in the header.
Anyway, I am putting the experiment in this branch for now.
That being said, the `Bigstep` declaration is way nicer with
`autoBoundImplicitLocal`s.

Another option is to add a new option `ctorAutoBoundImplicitLocal`
that is false by default, and activates auto implicit locals for
constructors when set to true.
 2021-02-02 10:18:21 -08:00
Sebastian Ullrich
b83875301a chore: move test without output 
/cc @leodemoura
 2021-02-02 13:37:56 +01:00
Sebastian Ullrich
dd6c291788 fix: relax eager mvar instantiation during constructor elaboration 
@leodemoura: Could you double-check?
 2021-02-02 13:19:15 +01:00
Leonardo de Moura
ac104213e3 test: cases-using name resolution issue 2021-02-01 13:16:19 -08:00
Sebastian Ullrich
d4dc54a724 fix: make sure to instantiate mvars in constructors 2021-02-01 12:10:26 +01:00
Leonardo de Moura
c4cfbceb71 test: div0 crash 2021-01-31 08:52:39 -08:00
Leonardo de Moura
b7a0bdb9c9 fix: Injection.lean 2021-01-30 11:58:56 -08:00
Leonardo de Moura
d71aab5dc4 fix: allow bigger ctor objects 
`IR/Checker.lean` is now also checking the maximum number of fields
and scalar size
 2021-01-29 18:23:38 -08:00
Leonardo de Moura
f1a0044241 fix: use previously generated sizeOf_spec lemmas to expand rhs 2021-01-27 18:14:25 -08:00
Leonardo de Moura
c47c25cf33 feat: finish sizeOf_spec lemma generation 2021-01-27 17:20:23 -08:00
Leonardo de Moura
17edc1d615 test: inductive types for testing SizeOf.lean 2021-01-27 16:26:03 -08:00
Leonardo de Moura
8b3a28dd2b test: reflection 2021-01-27 12:11:43 -08:00
Sebastian Ullrich
7e521f0105 chore: remove remaining #lang lean4 in tests 2021-01-27 14:45:31 +01:00
Sebastian Ullrich
a3a8d76e96 chore: move pp_options.cpp to Lean 2021-01-27 14:16:12 +01:00
Leonardo de Moura
2c05e78728 fix: bug at CheckAssignment 2021-01-26 16:20:41 -08:00
Leonardo de Moura
f53e83b182 feat: add options maxHeartbeats and synthInstance.maxHeartbeats 2021-01-24 17:45:50 -08:00